Formalization of Hoare logic

examples/hoare_logic/formula.why

+theory Formula
+
+type ident
+
+function mk_ident int : ident
+
+type fmla 'a =
+  | Ffalse
+  | Ftrue
+  | Fatom 'a
+  | Fnot (fmla 'a)
+  | Fand (fmla 'a) (fmla 'a)
+  | For (fmla 'a) (fmla 'a)
+  | Fimp (fmla 'a) (fmla 'a)
+  | Fiff (fmla 'a) (fmla 'a)
+  | Fforall ident (fmla 'a)
+  | Fexists ident (fmla 'a)
+
+end
+
+theory PropositionalCalculus
+
+use import bool.Bool
+use import Formula
+
+type prop_fmla = fmla ident
+
+use map.Map as IdMap
+
+type idmap 'a = IdMap.map ident 'a
+
+function eval (f:prop_fmla) (v:idmap bool) : bool =
+  match f with
+    | Ffalse -> False
+    | Ftrue -> True
+    | Fatom x -> IdMap.get v x
+    | Fnot p -> notb (eval p v)
+    | Fand p q -> andb (eval p v) (eval q v)
+    | For p q -> orb (eval p v) (eval q v)
+    | Fimp p q -> orb (notb (eval p v)) (eval q v)
+    | Fiff p q -> notb (xorb (eval p v) (eval q v))
+    | Fforall _ _ -> False
+    | Fexists _ _ -> False
+  end
+
+
+  goal Test1 :
+    let x = mk_ident 0 in
+    let v = IdMap.set (IdMap.const False) x True in
+    eval (For (Fnot (Fatom x)) (Ffalse)) v = False
+
+end
+
+

examples/hoare_logic/formula/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session SYSTEM "why3session.dtd">
+<why3session
+ name="formula/why3session.xml">
+ <prover
+  id="alt-ergo"
+  name="Alt-Ergo"
+  version="0.93"/>
+ <prover
+  id="coq"
+  name="Coq"
+  version="8.2pl1"/>
+ <prover
+  id="cvc3"
+  name="CVC3"
+  version="2.2"/>
+ <prover
+  id="eprover"
+  name="Eprover"
+  version="1.4 Namring"/>
+ <prover
+  id="gappa"
+  name="Gappa"
+  version="0.15.1"/>
+ <prover
+  id="simplify"
+  name="Simplify"
+  version="1.5.4"/>
+ <prover
+  id="spass"
+  name="Spass"
+  version="3.7"/>
+ <prover
+  id="vampire"
+  name="Vampire"
+  version="0.6"/>
+ <prover
+  id="verit"
+  name="veriT"
+  version="dev"/>
+ <prover
+  id="yices"
+  name="Yices"
+  version="1.0.25"/>
+ <prover
+  id="z3"
+  name="Z3"
+  version="2.19"/>
+ <file
+  name="../formula.why"
+  verified="true"
+  expanded="true">
+  <theory
+   name="Formula"
+   verified="true"
+   expanded="true">
+  </theory>
+  <theory
+   name="PropositionalCalculus"
+   verified="true"
+   expanded="true">
+   <goal
+    name="Test1"
+    sum="6bcc11f84daf50293f0fb99637a8f70a"
+    proved="true"
+    expanded="true"
+    shape="Lamk_identc0LasetaconstaFalseV0aTrueainfix =aevalaForaFnotaFatomV0aFfalseV1aFalse">
+    <proof
+     prover="cvc3"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.05"/>
+    </proof>
+    <proof
+     prover="alt-ergo"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.13"/>
+    </proof>
+    <proof
+     prover="vampire"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.59"/>
+    </proof>
+   </goal>
+  </theory>
+ </file>
+</why3session>

examples/hoare_logic/imp.why

+
+theory Imp
+
+type ident
+
+function mk_ident int : ident
+
+type operator = Oplus | Ominus | Omult
+
+type expr =
+  | Econst int
+  | Evar ident
+  | Ebin expr operator expr
+
+type stmt =
+  | Sskip
+  | Sassign ident expr
+  | Sseq stmt stmt
+  | Sif expr stmt stmt
+  | Swhile expr stmt
+
+lemma check_skip:
+  forall s:stmt. s=Sskip \/s<>Sskip
+
+use map.Map as IdMap
+use import int.Int
+
+type state = IdMap.map ident int
+
+function eval_bin (x:int) (op:operator) (y:int) : int =
+  match op with
+    | Oplus -> x+y
+    | Ominus -> x-y
+    | Omult -> x*y
+  end
+
+function eval_expr (s:state) (e:expr) : int =
+  match e with
+    | Econst n -> n
+    | Evar x -> IdMap.get s x
+    | Ebin e1 op e2 ->
+       eval_bin (eval_expr s e1) op (eval_expr s e2)
+  end
+
+  goal Test13 :
+    let s = IdMap.const 0 in
+    eval_expr s (Econst 13) = 13
+
+  goal Test42 :
+    let x = mk_ident 0 in
+    let s = IdMap.set (IdMap.const 0) x 42 in
+    eval_expr s (Evar x) = 42
+
+  goal Test55 :
+    let x = mk_ident 0 in
+    let s = IdMap.set (IdMap.const 0) x 42 in
+    eval_expr s (Ebin (Evar x) Oplus (Econst 13)) = 55
+
+
+(* small-steps semantics *)
+
+inductive one_step state stmt state stmt =
+
+  | one_step_assign:
+      forall s:state, x:ident, e:expr.
+        one_step s (Sassign x e)
+                 (IdMap.set s x (eval_expr s e)) Sskip
+
+  | one_step_seq:
+      forall s s':state, i1 i1' i2:stmt.
+        one_step s i1 s' i1' ->
+          one_step s (Sseq i1 i2) s' (Sseq i1' i2)
+
+  | one_step_seq_skip:
+      forall s:state, i:stmt.
+        one_step s (Sseq Sskip i) s i
+
+  | one_step_if_true:
+      forall s:state, e:expr, i1 i2:stmt.
+        eval_expr s e <> 0 ->
+          one_step s (Sif e i1 i2) s i1
+
+  | one_step_if_false:
+      forall s:state, e:expr, i1 i2:stmt.
+        eval_expr s e = 0 ->
+          one_step s (Sif e i1 i2) s i2
+
+  | one_step_while_true:
+      forall s:state, e:expr, i:stmt.
+        eval_expr s e <> 0 ->
+          one_step s (Swhile e i) s (Sseq i (Swhile e i))
+
+  | one_step_while_false:
+      forall s:state, e:expr, i:stmt.
+        eval_expr s e = 0 ->
+          one_step s (Swhile e i) s Sskip
+
+  goal Ass42 :
+    let x = mk_ident 0 in
+    let s = IdMap.const 0 in
+    forall s':state.
+      one_step s (Sassign x (Econst 42)) s' Sskip ->
+        IdMap.get s' x = 42
+
+  goal If42 :
+    let x = mk_ident 0 in
+    let s = IdMap.const 0 in
+    forall s1 s2:state, i:stmt.
+      one_step s
+        (Sif (Evar x)
+             (Sassign x (Econst 13))
+             (Sassign x (Econst 42)))
+        s1 i ->
+      one_step s1 i s2 Sskip ->
+        IdMap.get s2 x = 42
+
+  lemma progress:
+    forall s:state, i:stmt.
+      i <> Sskip ->
+      exists s':state, i':stmt. one_step s i s' i'
+
+
+ (* many steps of execution *)
+ inductive many_steps state stmt state stmt =
+   | many_steps_refl:
+     forall s:state, i:stmt. many_steps s i s i
+   | many_steps_trans:
+     forall s1 s2 s3:state, i1 i2 i3:stmt.
+       one_step s1 i1 s2 i2 ->
+       many_steps s2 i2 s3 i3 ->
+       many_steps s1 i1 s3 i3
+
+type fmla =
+  | Fterm expr
+
+predicate eval_fmla (s:state) (f:fmla) =
+  match f with
+  | Fterm e -> eval_expr s e <> 0
+  end
+
+type triple = T fmla stmt fmla
+
+predicate valid_triple (t:triple) =
+  match t with
+  | T p i q ->
+    forall s:state. eval_fmla s p ->
+      forall s':state. many_steps s i s' Sskip ->
+        eval_fmla s' q
+  end
+
+function subst_expr (e:expr) (x:ident) (t:expr) : expr =
+  match e with
+  | Econst _ -> e
+  | Evar y -> if x=y then t else e
+  | Ebin e1 op e2 -> Ebin (subst_expr e1 x t) op (subst_expr e2 x t)
+  end
+
+function subst (f:fmla) (x:ident) (t:expr) : fmla =
+  match f with
+  | Fterm e -> Fterm (subst_expr e x t)
+  end
+
+lemma eval_subst:
+  forall s:state, f:fmla, x:ident, t:expr.
+    eval_fmla s (subst f x t) -> eval_fmla (IdMap.set s x (eval_expr s t)) f
+
+(* Hoare logic rules *)
+
+lemma assign_rule:
+  forall q:fmla, x:ident, e:expr.
+  valid_triple (T (subst q x e) (Sassign x e) q)
+
+end
+
+

examples/hoare_logic/imp/imp_Imp_assign_rule_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Parameter ident : Type.
+
+Parameter mk_ident: Z -> ident.
+
+
+Inductive operator  :=
+  | Oplus : operator 
+  | Ominus : operator 
+  | Omult : operator .
+
+Inductive expr  :=
+  | Econst : Z -> expr 
+  | Evar : ident -> expr 
+  | Ebin : expr -> operator -> expr -> expr .
+
+Inductive stmt  :=
+  | Sskip : stmt 
+  | Sassign : ident -> expr -> stmt 
+  | Sseq : stmt -> stmt -> stmt 
+  | Sif : expr -> stmt -> stmt -> stmt 
+  | Swhile : expr -> stmt -> stmt .
+
+Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter const: forall (b:Type) (a:Type), b -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
+  b1):(map a b)) a1) = b1).
+
+Definition state  := (map ident Z).
+
+Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
+  match op with
+  | Oplus => (x + y)%Z
+  | Ominus => (x - y)%Z
+  | Omult => (x * y)%Z
+  end.
+
+Set Implicit Arguments.
+Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
+  match e with
+  | (Econst n) => n
+  | (Evar x) => (get s x)
+  | (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
+  end.
+Unset Implicit Arguments.
+
+Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
+  -> stmt -> Prop :=
+  | one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
+      (one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
+  | one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
+      (i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
+      i2) sqt (Sseq i1qt i2))
+  | one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
+      (Sseq Sskip i) s i)
+  | one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
+      (~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
+  | one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
+      (i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
+  | one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
+      (~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
+      (Swhile e i)))
+  | one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
+      ((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
+
+Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
+  exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
+
+Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
+  -> stmt -> Prop :=
+  | many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i)
+  | many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
+      ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
+      ((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
+
+Inductive fmla  :=
+  | Fterm : expr -> fmla .
+
+Definition eval_fmla(s:(map ident Z)) (f:fmla): Prop :=
+  match f with
+  | (Fterm e) => ~ ((eval_expr s e) = 0%Z)
+  end.
+
+Inductive triple  :=
+  | T : fmla -> stmt -> fmla -> triple .
+
+Definition valid_triple(t:triple): Prop :=
+  match t with
+  | (T p i q) => forall (s:(map ident Z)), (eval_fmla s p) ->
+      forall (sqt:(map ident Z)), (many_steps s i sqt Sskip) ->
+      (eval_fmla sqt q)
+  end.
+
+Parameter subst_expr: expr -> ident -> expr -> expr.
+
+
+Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
+  match e with
+  | (Econst _) => ((subst_expr e x t) = e)
+  | (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
+      ((subst_expr e x t) = e))
+  | (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
+      (subst_expr e2 x t)))
+  end.
+
+Definition subst(f:fmla) (x:ident) (t:expr): fmla :=
+  match f with
+  | (Fterm e) => (Fterm (subst_expr e x t))
+  end.
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem assign_rule : forall (q:fmla) (x:ident) (e:expr),
+  (valid_triple (T (subst q x e) (Sassign x e) q)).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intros q x e.
+unfold valid_triple.
+intros s Pre s' Hred.
+inversion Hred; subst.
+inversion H; subst.
+inversion H0; subst.
+(* normal case *)
+clear H Hred H0.
+apply subst_lemma.
+
+(* absurd case *)
+inversion H1.
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/hoare_logic/imp/imp_Imp_eval_subst_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Parameter ident : Type.
+
+Parameter mk_ident: Z -> ident.
+
+
+Inductive operator  :=
+  | Oplus : operator 
+  | Ominus : operator 
+  | Omult : operator .
+
+Inductive expr  :=
+  | Econst : Z -> expr 
+  | Evar : ident -> expr 
+  | Ebin : expr -> operator -> expr -> expr .
+
+Inductive stmt  :=
+  | Sskip : stmt 
+  | Sassign : ident -> expr -> stmt 
+  | Sseq : stmt -> stmt -> stmt 
+  | Sif : expr -> stmt -> stmt -> stmt 
+  | Swhile : expr -> stmt -> stmt .
+
+Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
+
+Parameter map : forall (a:Type) (b:Type), Type.
+
+Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
+
+Implicit Arguments get.
+
+Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
+
+Implicit Arguments set.
+
+Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
+  a2) = b1).
+
+Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
+  forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
+  a2) = (get m a2)).
+
+Parameter const: forall (b:Type) (a:Type), b -> (map a b).
+
+Set Contextual Implicit.
+Implicit Arguments const.
+Unset Contextual Implicit.
+
+Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
+  b1):(map a b)) a1) = b1).
+
+Definition state  := (map ident Z).
+
+Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
+  match op with
+  | Oplus => (x + y)%Z
+  | Ominus => (x - y)%Z
+  | Omult => (x * y)%Z
+  end.
+
+Set Implicit Arguments.
+Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
+  match e with
+  | (Econst n) => n
+  | (Evar x) => (get s x)
+  | (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
+  end.
+Unset Implicit Arguments.
+
+Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
+  -> stmt -> Prop :=
+  | one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
+      (one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
+  | one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
+      (i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
+      i2) sqt (Sseq i1qt i2))
+  | one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
+      (Sseq Sskip i) s i)
+  | one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
+      (~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
+  | one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
+      (i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
+  | one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
+      (~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
+      (Swhile e i)))
+  | one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
+      ((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
+
+Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
+  exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
+
+Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
+  -> stmt -> Prop :=
+  | many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i)
+  | many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
+      ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
+      ((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
+
+Inductive fmla  :=
+  | Fterm : expr -> fmla .
+
+Definition eval_fmla(s:(map ident Z)) (f:fmla): Prop :=
+  match f with
+  | (Fterm e) => ~ ((eval_expr s e) = 0%Z)
+  end.
+
+Inductive triple  :=
+  | T : fmla -> stmt -> fmla -> triple .
+
+Definition valid_triple(t:triple): Prop :=
+  match t with
+  | (T p i q) => forall (s:(map ident Z)), (eval_fmla s p) ->
+      forall (sqt:(map ident Z)), (many_steps s i sqt Sskip) ->
+      (eval_fmla sqt q)
+  end.
+
+Parameter subst_expr: expr -> ident -> expr -> expr.
+
+
+Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
+  match e with
+  | (Econst _) => ((subst_expr e x t) = e)
+  | (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
+      ((subst_expr e x t) = e))
+  | (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
+      (subst_expr e2 x t)))
+  end.
+
+Definition subst(f:fmla) (x:ident) (t:expr): fmla :=
+  match f with
+  | (Fterm e) => (Fterm (subst_expr e x t))
+  end.
+
+(* YOU MAY EDIT THE CONTEXT BELOW *)
+
+(* DO NOT EDIT BELOW *)
+
+Theorem eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
+  (eval_fmla s (subst f x t)) -> (eval_fmla (set s x (eval_expr s t)) f).
+(* YOU MAY EDIT THE PROOF BELOW *)
+intuition.
+
+Qed.
+(* DO NOT EDIT BELOW *)
+
+

examples/hoare_logic/imp/imp_Imp_progress_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Parameter ident : Type.
+
+Parameter mk_ident: Z -> ident.
+
+
+Inductive operator  :=
+  | Oplus : operator 
+  | Ominus : operator 
+  | Omult : operator .
+
+Inductive expr  :=
+  | Econst : Z -> expr 
+  | Evar : ident -> expr 
+  | Ebin : expr -> operator -> expr -> expr .
+
+Inductive stmt  :=
+  | Sskip : stmt 
+  | Sassign : ident -> expr -> stmt 
+  | Sseq : stmt -> stmt -> stmt 
+  | Sif : expr -> stmt -> stmt -> stmt 
+  | Swhile : expr -> stmt -> stmt .
+