Skip to content

GitLab

why3
why3
Commit 3b32bd70 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

matrix.Matrix: no more use of pairs 

Matrix.get and Matrix.set are now currified
no more matrix.MatrixSyntax
parent 6c548dc1
Hide whitespace changes
Inline Side-by-side
Showing with 118 additions and 119 deletions
examples/tests/matrix-test.mlw
View file @ 3b32bd70
module TestMatrix
use import int.Int
use import matrix.Syntax
use import matrix.Matrix
let test1 () =
let m1 = make 3 3 2 in
assert { m1[(0,0)] = 2 };
m1[(0,0)] <- 4;
assert { m1[(0,0)] = 4 };
assert { m1[(0,1)] = 2 };
assert { m1[(1,0)] = 2 };
assert { get m1 0 0 = 2 };
set m1 0 0 4;
assert { get m1 0 0 = 4 };
assert { get m1 0 1 = 2 };
assert { get m1 1 0 = 2 };
()
end
......
examples/warshall_algorithm.mlw
View file @ 3b32bd70
......@@ -18,7 +18,7 @@ module WarshallAlgorithm
inductive path (matrix bool) int int int =
| Path_empty:
forall m: matrix bool, i j k: int.
get m (i,j) -> path m i j k
get m i j -> path m i j k
| Path_cons:
forall m: matrix bool, i x j k: int.
0 <= x < k -> path m i x k -> path m x j k -> path m i j k
......@@ -35,26 +35,26 @@ module WarshallAlgorithm
requires { m.rows = m.columns }
ensures { let n = m.rows in
forall x y: int. 0 <= x < n -> 0 <= y < n ->
get result (x,y) <-> path m x y n }
get result x y <-> path m x y n }
=
let t = copy m in
let n = m.rows in
for k = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <-> path m x y k }
get t x y <-> path m x y k }
for i = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <->
get t x y <->
if x < i
then path m x y (k+1)
else path m x y k }
for j = 0 to n - 1 do
invariant { forall x y. 0 <= x < n -> 0 <= y < n ->
get t (x,y) <->
get t x y <->
if x < i \/ (x = i /\ y < j)
then path m x y (k+1)
else path m x y k }
set t (i,j) (get t (i,j) || get t (i,k) && get t (k,j))
set t i j (get t i j || get t i k && get t k j)
done
done
done;
......
examples/warshall_algorithm/warshall_algorithm_WarshallAlgorithm_weakening_1.v
View file @ 3b32bd70
......@@ -39,30 +39,18 @@ Definition rows {a:Type} {a_WT:WhyType a} (v:(matrix a)): Z :=
end.
(* Why3 assumption *)
Definition index := (Z* Z)%type.
Definition get {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (r:Z) (c:Z): a :=
(map.Map.get (map.Map.get (elts a1) r) c).
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z*
Z)%type): a :=
match i with
| (r, c) => (map.Map.get (map.Map.get (elts a1) r) c)
end.
Definition set {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (r:Z) (c:Z)
(v:a): (matrix a) := (mk_matrix (rows a1) (columns a1)
(map.Map.set (elts a1) r (map.Map.set (map.Map.get (elts a1) r) c v))).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z* Z)%type)
(v:a): (matrix a) :=
match i with
| (r, c) => (mk_matrix (rows a1) (columns a1) (map.Map.set (elts a1) r
(map.Map.set (map.Map.get (elts a1) r) c v)))
end.
(* Why3 assumption *)
Definition valid_index {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z*
Z)%type): Prop :=
match i with
| (r, c) => ((0%Z <= r)%Z /\ (r < (rows a1))%Z) /\ ((0%Z <= c)%Z /\
(c < (columns a1))%Z)
end.
Definition valid_index {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (r:Z)
(c:Z): Prop := ((0%Z <= r)%Z /\ (r < (rows a1))%Z) /\ ((0%Z <= c)%Z /\
(c < (columns a1))%Z).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (r:Z) (c:Z) (v:a): (matrix a) :=
......@@ -71,8 +59,8 @@ Definition make {a:Type} {a_WT:WhyType a} (r:Z) (c:Z) (v:a): (matrix a) :=
(* Why3 assumption *)
Inductive path: (matrix bool) -> Z -> Z -> Z -> Prop :=
| Path_empty : forall (m:(matrix bool)) (i:Z) (j:Z) (k:Z), ((get m (i,
j)) = true) -> (path m i j k)
| Path_empty : forall (m:(matrix bool)) (i:Z) (j:Z) (k:Z), ((get m i
j) = true) -> (path m i j k)
| Path_cons : forall (m:(matrix bool)) (i:Z) (x:Z) (j:Z) (k:Z),
((0%Z <= x)%Z /\ (x < k)%Z) -> ((path m i x k) -> ((path m x j k) ->
(path m i j k))).
......@@ -80,6 +68,7 @@ Inductive path: (matrix bool) -> Z -> Z -> Z -> Prop :=
(* Why3 goal *)
Theorem weakening : forall (m:(matrix bool)) (i:Z) (j:Z) (k1:Z) (k2:Z),
((0%Z <= k1)%Z /\ (k1 <= k2)%Z) -> ((path m i j k1) -> (path m i j k2)).
(* Why3 intros m i j k1 k2 (h1,h2) h3. *)
intros m i j k1 k2 (h1,h2) h3.
induction h3.
apply Path_empty; auto.
......
examples/warshall_algorithm/why3session.xml
View file @ 3b32bd70
......@@ -5,129 +5,162 @@
<prover id="0" name="Coq" version="8.4pl4" timelimit="6" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.3" timelimit="6" memlimit="1000"/>
<prover id="6" name="Z3" version="4.3.2" timelimit="6" memlimit="1000"/>
<file name="../warshall_algorithm.mlw" expanded="true">
<theory name="WarshallAlgorithm" sum="9398ff12771a26b5023a4309355f65dd" expanded="true">
<theory name="WarshallAlgorithm" sum="e403a7124488e8a32e9dedfabb4f54b4" expanded="true">
<goal name="weakening" expanded="true">
<proof prover="0" edited="warshall_algorithm_WarshallAlgorithm_weakening_1.v"><result status="valid" time="0.97"/></proof>
<proof prover="0" edited="warshall_algorithm_WarshallAlgorithm_weakening_1.v"><result status="valid" time="0.77"/></proof>
</goal>
<goal name="decomposition" expanded="true">
<proof prover="0" edited="warshall_algorithm_WarshallAlgorithm_decomposition_1.v"><result status="valid" time="1.53"/></proof>
<proof prover="0" edited="warshall_algorithm_WarshallAlgorithm_decomposition_1.v"><result status="valid" time="1.18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure" expl="VC for transitive_closure">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure" expl="VC for transitive_closure" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter transitive_closure.1" expl="1. postcondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.2" expl="2. loop invariant init">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.3" expl="3. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.4" expl="4. loop invariant init">
<proof prover="2"><result status="valid" time="0.08"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.08"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.5" expl="5. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.5.1" expl="1. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.5.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.5.3" expl="3. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.6" expl="6. loop invariant init">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="50"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.7" expl="7. type invariant">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.8" expl="8. precondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.9" expl="9. precondition">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.10" expl="10. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.10.1" expl="1. loop invariant preservation">
<transf name="split_all_full">
<goal name="WP_parameter transitive_closure.10.1.1" expl="1. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.10.1.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="49"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.10.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="38"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.10.3" expl="3. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="82"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.11" expl="11. precondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.12" expl="12. precondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.13" expl="13. precondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.14" expl="14. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.14.1" expl="1. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.15"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.14.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="43"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.14.3" expl="3. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.07"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="0.07"/></proof>
<proof prover="3"><result status="timeout" time="5.98"/></proof>
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.15" expl="15. precondition">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.16" expl="16. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.16.1" expl="1. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="1" obsolete="true"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.16.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="41"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.16.3" expl="3. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.17" expl="17. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.10"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.10"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="55"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.18" expl="18. loop invariant preservation">
<transf name="split_goal_wp">
<goal name="WP_parameter transitive_closure.18.1" expl="1. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="18"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.18.2" expl="2. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter transitive_closure.19" expl="19. type invariant">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter transitive_closure.20" expl="20. postcondition">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="2" obsolete="true"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
</transf>
</goal>
......
modules/matrix.mlw
View file @ 3b32bd70
......@@ -9,26 +9,23 @@ module Matrix
model { rows: int; columns: int; mutable elts: map int (map int 'a) }
invariant { 0 <= self.rows /\ 0 <= self.columns }
type index = (int, int)
function get (a: matrix 'a) (r c: int) : 'a =
M.get (M.get a.elts r) c
function get (a: matrix 'a) (i: index) : 'a =
let r,c = i in M.get (M.get a.elts r) c
function set (a: matrix 'a) (i: index) (v: 'a) : matrix 'a =
let r,c = i in
function set (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a =
{ a with elts = M.set a.elts r (M.set (M.get a.elts r) c v) }
predicate valid_index (a: matrix 'a) (i: index) =
let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns
predicate valid_index (a: matrix 'a) (r c: int) =
0 <= r < a.rows /\ 0 <= c < a.columns
val get (a: matrix 'a) (i: index) : 'a
requires { valid_index a i }
ensures { result = get a i }
val get (a: matrix 'a) (r c: int) : 'a
requires { valid_index a r c }
ensures { result = get a r c }
val set (a: matrix 'a) (i: index) (v: 'a) : unit writes {a}
requires { valid_index a i }
ensures { let r,c = i in
a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }
val set (a: matrix 'a) (r c: int) (v: 'a) : unit
requires { valid_index a r c }
writes {a}
ensures { a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v)}
val rows (a: matrix 'a) : int ensures { result = a.rows }
val columns (a: matrix 'a) : int ensures { result = a.columns }
......@@ -36,52 +33,32 @@ module Matrix
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
let defensive_get (a: matrix 'a) (i: index)
ensures { valid_index a i /\ result = get a i }
raises { OutOfBounds -> not (valid_index a i) }
= let r,c = i in
if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
get a i
let defensive_get (a: matrix 'a) (r c: int) : 'a
ensures { valid_index a r c }
ensures { result = get a r c }
raises { OutOfBounds -> not (valid_index a r c) }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
get a r c
let defensive_set (a: matrix 'a) (i: index) (v: 'a)
ensures { valid_index a i /\ a = set (old a) i v }
raises { OutOfBounds -> not (valid_index a i) /\ a = old a }
= let r,c = i in
if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
set a i v
let defensive_set (a: matrix 'a) (r c: int) (v: 'a) : unit
ensures { valid_index a r c }
ensures { a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v)}
raises { OutOfBounds -> not (valid_index a r c) /\ a = old a }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
set a r c v
function make (r c: int) (v: 'a) : matrix 'a =
{ rows = r; columns = c; elts = M.const (M.const v) }
val make (r c: int) (v: 'a) : matrix 'a
requires { r >= 0 /\ c >= 0 } ensures { result = make r c v }
requires { r >= 0 /\ c >= 0 }
ensures { result = make r c v }
val copy (a: matrix 'a) : matrix 'a
ensures { result.rows = a.rows /\ result.columns = a.columns }
ensures { forall r:int. 0 <= r < result.rows ->
forall c:int. 0 <= c < result.columns ->
get result (r,c) = get a (r,c) }
end
(* {2 Square bracket syntax in both logic and programs} *)
module Syntax
use import int.Int
use export Matrix
function ([]) (a: matrix 'a) (i: index) : 'a = get a i
function ([<-]) (a: matrix 'a) (i: index) (v: 'a) : matrix 'a = set a i v
val ([]) (a: matrix 'a) (i: index) : 'a
requires { valid_index a i }
ensures { result = get a i }
val ([]<-) (a: matrix 'a) (i: index) (v: 'a) : unit writes {a}
requires { let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns }
ensures { let r,c = i in
a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }
get result r c = get a r c }
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment