ExpressionAbbrevs.v 573 Bytes
Newer Older
Heiko Becker's avatar
Heiko Becker committed
1
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals.
2
3
Require Export Daisy.Infra.Abbrevs Daisy.Expressions.

Heiko Becker's avatar
Heiko Becker committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Definition analysisResult :Type := exp Q -> intv * error.


Definition envApproximatesPrecond (P:nat -> intv) (absenv:analysisResult) :=
  forall u:nat,
    let (ivlo,ivhi) := P u in
    let (absIv,err) := absenv (Param Q u) in
    let (abslo,abshi) := absIv in
    (abslo <= ivlo /\ ivhi <= abshi)%Q.

Definition precondValidForExec (P:nat->intv) (cenv:nat->R) :=
  forall v:nat,
    let (ivlo,ivhi) := P v in
    (Q2R ivlo <= cenv v <= Q2R ivhi)%R.