vm_ex_assignment

vm_ex_assignment.mlw

+module Vm_Ex
+
+  use vm.Vm
+  use option.Option
+  use int.Int
+  use list.List
+  use list.Length
+  use list.Append
+  use list.Nth
+  use list.NthLength
+  use state.State
+  use state.Reg
+  use bv_op.BV_OP
+
+  exception Err
+  exception Halt machine_state
+ 
+  lemma codeseq_at_zero:
+    forall c1 c2. length c1 = 0 -> 
+      codeseq_at (c1 ++ c2) 0 c2
+
+  let rec split_at p (c:code)   
+    raises   { Err ->  p >= length c }
+
+    requires { p >= 0 } (* well founded *)
+    variant  { p }      (* termination  *)
+
+    ensures  { 
+        let (hd, tl) = result in
+        hd ++ tl = c /\
+        codeseq_at c p tl /\
+        length tl > 0
+    }
+  = match (c, p = 0) with
+    | (Nil, _)       -> raise Err (* p >= length c *)
+    | (_, True)      -> (Nil, c)
+    | (Cons e c', _) -> 
+      let (hd, tl) = split_at (p - 1) c' in
+      (Cons e hd, tl)
+    end
+
+  let pop (s:stack) : (int, stack)
+    ensures {
+      let (rv, rs) = result in
+      Cons rv rs  = s (* original stack *)
+    }
+    raises { Err }
+  =
+    match s with
+    | Nil        -> raise Err
+    | Cons rv rs -> (rv, rs)
+    end
+
+  let instr_ex (c: code) (ms: machine_state): machine_state 
+    raises   { Err }
+    raises   { Halt (VMS p _ _ _) -> codeseq_at c p ihalt }
+    ensures  { transition c ms result } 
+  =
+    let VMS p r s m = ms in (* split machine state *)
+    
+    if p < 0 then raise Err;
+
+    try 
+      let (_, Cons instr _) = split_at p c in      
+      assert { codeseq_at c p (Cons instr Nil)};
+    
+      match instr with      
+      
+      | Iconst n    -> (*   push n on stack                               *)
+        VMS (p + 1) r (push n s) m 
+        
+    
+      | Ihalt -> raise (Halt ms)
+      
+      (* your code here *)
+    
+      | _ -> raise Err
+      end
+    with 
+      Err -> raise Err  
+    end
+          
+  let rec instr_iter_ex (c: code) (ms: machine_state): machine_state 
+    raises   { Err }
+    raises   { Halt (VMS p _ _ _) -> codeseq_at c p ihalt }
+    ensures  { transition_star c ms result } 
+    diverges
+  =
+    instr_iter_ex c (instr_ex c ms)   
+   
+end
\ No newline at end of file

vm_ex_assignment/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="5">
+<prover id="0" name="Z3" version="4.7.1" alternative="counterexamples" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="1" name="Eprover" version="2.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="1000"/>
+<file name="../vm_ex_assignment.mlw" proved="true">
+<theory name="Vm_Ex" proved="true">
+ <goal name="codeseq_at_zero" proved="true">
+ <proof prover="1"><result status="valid" time="0.19"/></proof>
+ </goal>
+ <goal name="VC split_at" expl="VC for split_at" proved="true">
+ <transf name="split_vc" proved="true" >
+  <goal name="VC split_at.0" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.03" steps="76"/></proof>
+  </goal>
+  <goal name="VC split_at.1" expl="postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.04" steps="86"/></proof>
+  </goal>
+  <goal name="VC split_at.2" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.03" steps="77"/></proof>
+  </goal>
+  <goal name="VC split_at.3" expl="variant decrease" proved="true">
+  <proof prover="2"><result status="valid" time="0.03" steps="77"/></proof>
+  </goal>
+  <goal name="VC split_at.4" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.03" steps="77"/></proof>
+  </goal>
+  <goal name="VC split_at.5" expl="postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.14" steps="348"/></proof>
+  </goal>
+  <goal name="VC split_at.6" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.03" steps="82"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="VC pop" expl="VC for pop" proved="true">
+ <proof prover="2"><result status="valid" time="0.04" steps="74"/></proof>
+ </goal>
+ <goal name="VC instr_ex" expl="VC for instr_ex" proved="true">
+ <transf name="split_vc" proved="true" >
+  <goal name="VC instr_ex.0" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.03" steps="76"/></proof>
+  </goal>
+  <goal name="VC instr_ex.1" expl="assertion" proved="true">
+  <proof prover="0"><result status="valid" time="0.07"/></proof>
+  </goal>
+  <goal name="VC instr_ex.2" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.04"/></proof>
+  <proof prover="2"><result status="timeout" time="10.00"/></proof>
+  </goal>
+  <goal name="VC instr_ex.3" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.04" steps="82"/></proof>
+  </goal>
+  <goal name="VC instr_ex.4" expl="unreachable point" proved="true">
+  <proof prover="2"><result status="valid" time="0.04" steps="79"/></proof>
+  </goal>
+ </transf>
+ </goal>
+ <goal name="VC instr_iter_ex" expl="VC for instr_iter_ex" proved="true">
+ <proof prover="2"><result status="valid" time="0.06" steps="114"/></proof>
+ </goal>
+</theory>
+</file>
+</why3session>