Library simpleAssign
Require Import evidence.
Require Import soundnessProof.
Require Import soundness.
Require Import evidenceGenerator.
Require Import varLists.
Require Import soundnessProof.
Require Import soundness.
Require Import evidenceGenerator.
Require Import varLists.
Very simple example file
Definition x := AId 0.
Definition w := AId 1.
Definition wAgree := [(BvalExpr true, AExp (SvarExpr w))].
Definition xAgree := [(BvalExpr true, AExp (SvarExpr x))].
Definition cmd := (Assign (ASkalVar x) (AExp (SvarExpr w))).
Definition X := [ASkalVar x, ASkalVar w].
Definition assignEvid : TEvid X cmd (Assns
wAgree xAgree)
:=
TAAssignE X xAgree (ASkalVar x) (SvarExpr w) (eq_refl _) (eq_refl _).
Check assignEvid.
Definition evidSound := soundnessProof _ _ _ assignEvid.
Check evidSound.
Definition a := generatePrecondition cmd xAgree [].
Check a.
Definition pre := fst a.
Definition Y := snd a.
Definition aEvid := generatePreconditionEvidence cmd Y Y [] xAgree pre (eq_refl a)
(allVarsInRefl _).
Check aEvid.
Print aEvid.
Definition aEvidSound := soundnessProof _ _ _ aEvid.
Check aEvidSound.