Update examples in progress

doc/manual.tex

@@ -263,7 +263,24 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
 
 \chapter{Release Notes}
 
-\section{Release Notes for version 0.90: syntax changes w.r.t. 0.87}
+\section{Release Notes for version 0.90}
+
+TO DISCUSS:
+
+Pourquoi les lemma functions generent un warning ``does not contain any
+abstract symbol'' ?
+
+comment mettre a jour l'example bag ? Parametrer par une egalit'e sur
+les elements ?
+
+
+Attention, ne pas introduire 1 variable par champ complique le boulot des prouveurs
+
+``inline'' ne doit pas inliner Map.set
+
+egalite sur les type algebriques ? engendrees automatiquement ?
+
+\subsection{Syntax Changes}
 
 \begin{center}
   \begin{tabular}{|c|c|}
@@ -272,12 +289,27 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
 \hline
 \texttt{'L:} & \texttt{label L in} \\
 \texttt{at !x 'L} & \texttt{!x at L} \\
-\verb|\|\texttt{ x. t} & \texttt{fun x -> t} \\
-\texttt{type t model ...} & \texttt{type t = private ... } \\
+\verb|\|\texttt{ x. e} & \texttt{fun x -> e} \\
+\verb|\|\texttt{use HighOrd} & nothing, not needed anymore \\
+\verb|\|\texttt{HighOrd.pred ty} & \texttt{ty -> bool} \\
+\texttt{type t model ...} & \texttt{type t = abstract ... } \\
 \hline
   \end{tabular}
 \end{center}
 
+\subsection{Model types, abstract types}
+
+explain \texttt{private} and ghost fields, \texttt{abstract mutable},
+\texttt{private mutable}
+
+\subsection{Polymorphic Equality}
+
+No polymorphic equality in programs. Consequence : no List.mem in
+programs, need for List.mem, List.filter, parameterized with a
+predicate.
+
+No default equality on algebraic datatypes
+
 \section{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
 
 The syntax of \whyml programs changed in release 0.80.

examples/avl/association_list.mlw

@@ -14,7 +14,6 @@ module Assoc
   use import list.Mem
   use import list.Append
   use import option.Option
-  use import HighOrd
 
   (** Existence of an element identified by key [k] in list [l]. *)
   predicate appear (k:key) (l:list (t 'a)) =
@@ -181,4 +180,3 @@ module AssocSorted
   = ()
 
 end
-

examples/avl/avl.mlw

@@ -67,7 +67,6 @@ module AVL
   use import bool.Bool
   use import list.List
   use import list.Append
-  use import HighOrd
   use import option.Option
   use import ref.Ref
 
@@ -723,4 +722,3 @@ module AVL
     end
 
 end
-

examples/avl/monoid.mlw

@@ -25,7 +25,6 @@ module MonoidSum
 
   use import list.List
   use import list.Append
-  use import HighOrd
   clone import Monoid as M
 
   (** Axiomatized definition of the monoidal aggregation of elements
@@ -48,7 +47,6 @@ end
 (** {2 Definition of aggregation} *)
 module MonoidSumDef
   use import list.List
-  use import HighOrd
 
   namespace M
     type t
@@ -76,4 +74,3 @@ module ComputableMonoid
   val op (a b:t) : t ensures { result = op a b }
 
 end
-

examples/binary_multiplication.mlw

 
 module BinaryMultiplication
 
-  use import mach.int.Int
-  use import number.Parity
+  use import int.Int
+  use import int.ComputerDivision
   use import ref.Ref
 
   let binary_mult (a b: int)
@@ -15,11 +15,10 @@ module BinaryMultiplication
       invariant { 0 <= !y }
       invariant { !z + !x * !y = a * b }
       variant   { !y }
-      if odd !y then z := !z + !x;
+      if mod !y 2 <> 0 then z := !z + !x;
       x := 2 * !x;
-      y := !y / 2
+      y := div !y 2
     done;
     !z
 
 end
-

examples/binary_multiplication/why3session.xml

@@ -2,11 +2,48 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="4">
-<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="11" memlimit="1000"/>
+<prover id="1" name="Alt-Ergo" version="1.01" timelimit="5" memlimit="1000"/>
 <file name="../binary_multiplication.mlw" expanded="true">
-<theory name="BinaryMultiplication" sum="9c13d5392381b04161f82c19fb28f95e" expanded="true">
- <goal name="WP_parameter binary_mult" expl="VC for binary_mult" expanded="true">
- <proof prover="0"><result status="valid" time="0.74" steps="88"/></proof>
+<theory name="BinaryMultiplication" sum="782bbe968e92df7214b9a29b499aca45" expanded="true">
+ <goal name="VC binary_mult" expl="VC for binary_mult" expanded="true">
+ <transf name="split_goal_wp" expanded="true">
+  <goal name="VC binary_mult.1" expl="1. loop invariant init">
+  <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+  </goal>
+  <goal name="VC binary_mult.2" expl="2. loop invariant init">
+  <proof prover="1"><result status="valid" time="0.00" steps="1"/></proof>
+  </goal>
+  <goal name="VC binary_mult.3" expl="3. precondition">
+  <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
+  </goal>
+  <goal name="VC binary_mult.4" expl="4. precondition">
+  <proof prover="1"><result status="valid" time="0.01" steps="7"/></proof>
+  </goal>
+  <goal name="VC binary_mult.5" expl="5. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.01" steps="13"/></proof>
+  </goal>
+  <goal name="VC binary_mult.6" expl="6. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.07" steps="16"/></proof>
+  </goal>
+  <goal name="VC binary_mult.7" expl="7. loop variant decrease">
+  <proof prover="1"><result status="valid" time="0.02" steps="13"/></proof>
+  </goal>
+  <goal name="VC binary_mult.8" expl="8. precondition">
+  <proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
+  </goal>
+  <goal name="VC binary_mult.9" expl="9. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
+  </goal>
+  <goal name="VC binary_mult.10" expl="10. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
+  </goal>
+  <goal name="VC binary_mult.11" expl="11. loop variant decrease">
+  <proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
+  </goal>
+  <goal name="VC binary_mult.12" expl="12. postcondition">
+  <proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
+  </goal>
+ </transf>
  </goal>
 </theory>
 </file>

examples/bitcount.mlw

@@ -253,7 +253,6 @@ module Hamming
   use import int.NumOf
   use import mach.bv.BVCheck32
   use import BitCounting32
-  use import HighOrd as HO
 
   predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i
 
@@ -276,7 +275,7 @@ module Hamming
   =
     assert { hammingD_logic a b = 0 -> eq_sub a b 0 32 }
 
-  function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x
+  function fun_or (f g : 'a -> bool) : 'a -> bool = fun x -> f x \/ g x
 
   let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
     variant {b - a}
@@ -337,9 +336,7 @@ module AsciiCode
 
   (* use Numofbit *)
 
-  use HighOrd as HO
-
-  function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x
+  function fun_or (f g : 'a -> bool) : 'a -> bool = fun x -> f x \/ g x
 
   let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
     requires { forall i. a <= i < b -> not (p i) \/ not (q i) }
@@ -369,7 +366,7 @@ module AsciiCode
     ensures  { eq_sub_bv result b zeros lastbit }
     ensures  { validAscii result }
     let c = count b in
-    let maskbit = lsl_check c lastbit in
+    let maskbit = lsl_check c (of_int 31) in
     assert { bw_and b maskbit = zeros };
     assert { even (to_uint c) ->
                not (nth_bv c zeros)

examples/bitwalker.mlw

@@ -28,7 +28,8 @@ module Bitwalker
       BV8.nth value i = BV8.nth_bv value (C8_32.toSmall (BV32.of_int i))
 
   (*  *)
-  function maxvalue (len : BV32.t) : BV64.t = BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)
+  let function maxvalue (len : BV32.t) : BV64.t =
+    BV64.lsl_bv (BV64.of_int 1) (C32_64.toBig len)
 
   let lemma nth_ultpre0 (x:BV64.t) (len:BV32.t)
     requires { BV32.to_uint len < 64}
@@ -106,7 +107,7 @@ module Bitwalker
     let mask =
       BV32.lsl_bv (BV32.int_check 1) (BV32.sub_check (BV32.int_check 7) left)
     in
-    BV32.bw_and (C8_32.toBig byte) mask <> BV32.zeros
+    not (BV32.eq (BV32.bw_and (C8_32.toBig byte) mask) BV32.zeros)
     end
 
   (* return the bit of the [left]/8 element of [addr] at position mod [left] 8 starting from the left *)
@@ -172,7 +173,7 @@ module Bitwalker
                        (BV64.sub (BV64.of_int 63) (C32_64.toBig left))}
        let mask = BV64.lsl_bv (BV64.int_check 1)
                   (C32_64.toBig (BV32.sub_check (BV32.int_check 63) left)) in
-       BV64.bw_and value mask <> BV64.zeros
+       not (BV64.eq (BV64.bw_and value mask) BV64.zeros)
      end
 
 (*
@@ -253,18 +254,18 @@ module Bitwalker
     let lstart = BV32.sub_check (BV32.of_int 64) len in
     let i = ref BV32.zeros in
 
-    'Init:
+    label Init in
     while BV32.ult !i len do variant { !i with BV32.ugt }
     invariant {0 <= BV32.to_uint !i <= BV32.to_uint len}
     invariant {forall j:int. 0 <= j < BV32.to_uint start ->
-                 nth8_stream (at addr 'Init) j
+                 nth8_stream (addr at Init) j
                = nth8_stream addr j}
     invariant {forall j:int. BV32.to_uint start <= j < BV32.to_uint start + BV32.to_uint !i ->
                  nth8_stream addr j
                = BV64.nth value (BV32.to_uint len - j - 1 + BV32.to_uint start) }
     invariant {forall j:int. BV32.to_uint start + BV32.to_uint !i <= j < 8 * length addr ->
                  nth8_stream addr j
-               = nth8_stream (at addr 'Init) j }
+               = nth8_stream (addr at Init) j }
 
       let flag = peek_64bit value (BV32.add_check lstart !i) in
 
@@ -291,7 +292,7 @@ module Bitwalker
     ensures {forall i. 0 <= i < 8 * length addr ->
                nth8_stream addr i = nth8_stream (old addr) i}
   =
-    'Init:
+    label Init in
     let value = peek start len addr in
     let res = poke start len addr value in
 
@@ -299,7 +300,7 @@ module Bitwalker
 
     assert {forall i. BV32.to_uint start <= i < BV32.to_uint start + BV32.to_uint len ->
          nth8_stream addr i
-       = nth8_stream (at addr 'Init) i};
+       = nth8_stream (addr at Init) i};
 
     res
 

examples/bts/16972.mlw

 
 module M
 
-  use import HighOrd
-
   type t = A | B
   type s = { field1 : t -> t ; field2 : t -> t }
 

examples/defunctionalization.mlw

@@ -143,8 +143,6 @@ use import Expr
 
 *)
 
-use HighOrd
-
 function eval_1 (e:expr) (k: int->'a) : 'a =
   match e with
     | Cte n -> k n
@@ -480,8 +478,6 @@ function interpret_0 (p:prog) : value = eval_0 p
 *)
 
 
-use HighOrd
-
 function eval_1 (e:expr) (k:value -> 'a) : 'a =
   match e with
     | Cte n -> k (if n >= 0 then Vnum n else Underflow)

examples/double_wp/logic.mlw

@@ -9,8 +9,6 @@ module Compiler_logic
   use import list.Append
   use import vm.Vm
   use import state.State
-  use import HighOrd
-
 
   function fst (p: ('a,'b)) : 'a = let (x,_) = p in x
   meta rewrite_def function fst
@@ -166,4 +164,3 @@ module Compiler_logic
     res
 
 end
-

examples/double_wp/specs.mlw

@@ -8,7 +8,6 @@ module VM_instr_spec
   use import list.Length
   use import vm.Vm
   use import state.State
-  use import HighOrd
   use import logic.Compiler_logic
 
   function ifun_post (f:machine_state -> machine_state) : post 'a =
@@ -218,4 +217,3 @@ module VM_instr_spec
     hoare isetvar_pre c (isetvar_post x)
 
 end
-

examples/hackers-delight.mlw

@@ -102,8 +102,6 @@ module Utils_Spec
 
   (** {6 hammingD correctness } *)
 
-  use HighOrd as HO
-
   predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i
 
   (** The correctness property can be express as the following: *)

examples/in_progress/cek.mlw

@@ -58,8 +58,6 @@ constant p2 : term =
            (Lambda y (Var y)))
       (Lambda x (Var x))
 
-use HighOrd as H
-
 predicate ground_rec (t:term) (bound: H.pred identifier) =
   match t with
   | Var v -> bound v
@@ -123,7 +121,7 @@ let rec lemma weak_nf_complete (t:term)
 = match t with
   | Var _ -> ()
   | Lambda _ _ -> ()
-  | App t1 t2 -> 
+  | App t1 t2 ->
     weak_nf_complete t1; weak_nf_complete t2
   end
 
@@ -132,7 +130,7 @@ let rec lemma weak_nf_complete (t:term)
 inductive weak_n_reduce int term term =
   | Zero : forall t. weak_n_reduce 0 t t
   | Succ : forall t1 t2 t3 n.
-     weak_reduce t1 t2 -> weak_n_reduce n t2 t3 -> 
+     weak_reduce t1 t2 -> weak_n_reduce n t2 t3 ->
      weak_n_reduce (n+1) t1 t3
 
 predicate weak_normalize (t1 t2:term) =
@@ -218,9 +216,9 @@ let rec lemma recompose_values (c:context) (t1 t2:expr) (e:environment) : unit
 </pre></blockquote>}
 *)
 
-let rec eval (t:term) (e:environment) (c:context) : value 
+let rec eval (t:term) (e:environment) (c:context) : value
   diverges
-  returns { Closure x t1 e1 -> 
+  returns { Closure x t1 e1 ->
     weak_normalize (recompose c t e) (Lambda x t1) }
 = match t with
   | Var x -> cont c (lookup x e)
@@ -228,7 +226,7 @@ let rec eval (t:term) (e:environment) (c:context) : value
   | App t0 t1 -> eval t0 e (Left c t1 e)
   end
 
-with cont (c:context) (v:value) : value 
+with cont (c:context) (v:value) : value
   diverges
 = match c with
   | Empty -> v
@@ -244,13 +242,9 @@ let compute p : value
     e = Nil /\ weak_normalize p (Lambda x t) }
 = eval p Nil Empty
 
-let test () 
-  diverges 
+let test ()
+  diverges
 = (compute p0,compute p1,compute p2)
 
 
 end
-
-
-
-

examples/in_progress/immutable_string.mlw

@@ -2,7 +2,6 @@
 module String
 
   use import int.Int
-  use HighOrd as HO
 
   type char
   constant dummy_char: char

examples/need_update/bag.mlw

 
 module Bag
 
-  use import HighOrd
   use import int.Int
 
   type bag 'a = 'a -> int

examples/patience.mlw

@@ -51,7 +51,6 @@ module PigeonHole
 *)
 
   use import int.Int
-  use HighOrd
 
   predicate range (f: int -> int) (n: int) (m:int) =
     forall i: int. 0 <= i < n -> 0 <= f i < m

examples/pigeonhole.mlw

@@ -5,7 +5,6 @@
 
 module Pigeonhole
 
-  use import HighOrd
   use import int.Int
   use import set.Fset
   use import ref.Ref

examples/register_allocation.mlw

@@ -7,7 +7,6 @@
 
 module Spec
 
-  use import HighOrd
   use import int.Int
 
   type addr
@@ -170,7 +169,6 @@ end
 
 module InfinityOfRegisters
 
-  use import HighOrd
   use import int.Int
   use import list.List
   use import list.Append
@@ -206,7 +204,6 @@ end
 
 module FiniteNumberOfRegisters
 
-  use import HighOrd
   use import int.Int
   use import list.List
   use import list.Append
@@ -246,7 +243,6 @@ end
 
 module OptimalNumberOfRegisters
 
-  use import HighOrd
   use import int.Int
   use import int.MinMax
   use import list.List

examples/tree_height.mlw

@@ -8,7 +8,6 @@ module HeightCPS
   use import int.MinMax
   use import bintree.Tree
   use import bintree.Height
-  use HighOrd
 
   function height_cps (t: tree 'a) (k: int -> 'b) : 'b =
     match t with
@@ -145,4 +144,3 @@ module HeightStack
   = height_stack 0 (Cons (0, t) Nil)
 
 end
-

share/strategies.conf

@@ -16,30 +16,33 @@ desc = "A@ simple@ blaster"
 shortcut = "b"
 code = "
 start:
-  c Alt-Ergo,0.95.2, 1 1000
+  c Alt-Ergo,1.01, 1 1000
   c CVC4,1.4, 1 1000
   t split_goal_wp start
-  c Alt-Ergo,0.95.2, 10 4000
+  c Alt-Ergo,1.01, 10 4000
   c CVC4,1.4, 10 4000"
 
 [strategy]
 name = "Mega Blaster"
 desc = "Mega@ Blaster@ of@ the@ death"
 code = "
-L0:c Alt-Ergo,0.95.2, 1 1000
+L0:c Alt-Ergo,1.01, 1 1000
    c CVC4,1.4, 1 1000
+   c Z3,4.4.1, 1 1000
    t split_goal_wp L6
    t introduce_premises L4
 L4:t inline_goal L0
    g L11
-L6:c Alt-Ergo,0.95.2, 1 1000
+L6:c Alt-Ergo,1.01, 1 1000
    c CVC4,1.4, 1 1000
+   c Z3,4.4.1, 1 1000
    t introduce_premises L9
 L9:t inline_goal L0
    t split_goal_wp L6
 L11:
-   c Alt-Ergo,0.95.2, 5 2000
+   c Alt-Ergo,1.01, 5 2000
    c CVC4,1.4, 5 2000
-   c Alt-Ergo,0.95.2, 30 4000
-   c CVC4,1.4, 30 4000"
-
+   c Z3,4.4.1, 5 2000
+   c Alt-Ergo,1.01, 30 4000
+   c CVC4,1.4, 30 4000
+   c Z3,4.4.1, 30 4000"

theories/bv.why

@@ -390,9 +390,12 @@ theory BV_Gen
 
   axiom Extensionality: forall x y : t [eq x y]. eq x y -> x = y
 
+  val eq (v1 v2 : t) : bool
+    ensures { if result then v1 = v2 else v1 <> v2 }
+
 end
 
-(** {2 Bit Vectors of common size_bvs, 8/16/32/64} *)
+(** {2 Bit Vectors of common sizes, 8/16/32/64} *)
 
 theory BV64
   constant size           : int = 64
@@ -466,8 +469,8 @@ theory BVConverter_Gen
   function to_uint_small smallBV : int
   function to_uint_big bigBV : int
 
-  function toBig smallBV : bigBV
-  function toSmall bigBV : smallBV
+  val function toBig smallBV : bigBV
+  val function toSmall bigBV : smallBV
 
   axiom toSmall_to_uint :
     forall x:bigBV. in_small_range x ->

theories/graph.why

@@ -49,7 +49,7 @@ theory IntPathWeight
   use import list.List
   use import list.Append
 
-  function weight vertex vertex : int
+  val function weight vertex vertex : int
 
   function path_weight (l: list vertex) (dst: vertex) : int = match l with
     | Nil -> 0

theories/list.why

@@ -28,6 +28,26 @@ theory Length
 
 end
 
+(** {2 Quantifiers on lists} *)
+
+module Quant
+
+  use import List
+
+  let rec function for_all (p: 'a -> bool) (l:list 'a) : bool =
+    match l with
+    | Nil -> true
+    | Cons x r -> p x && for_all p r
+    end
+
+  let rec function for_some (p: 'a -> bool) (l:list 'a) : bool =
+    match l with
+    | Nil -> true
+    | Cons x r -> p x || for_some p r
+    end
+
+end
+
 (** {2 Membership in a list} *)
 
 theory Mem
@@ -517,6 +537,8 @@ theory Sum
 
 end
 
+(* TODO: redesign these modules using higher-order instead
+
 (** {2 Induction on lists} *)
 
 theory Induction
@@ -585,6 +607,7 @@ theory FoldRight
     end
 
 end
+*)
 
 (** {2 Importation of all list theories in one} *)