Commit 273dcaff authored by Jean-Christophe's avatar Jean-Christophe

cleaning up for demos

parent 2b811033
...@@ -23,16 +23,12 @@ back +-+-+-+-------------------+ ...@@ -23,16 +23,12 @@ back +-+-+-+-------------------+
use import int.Int use import int.Int
use import module array.Array as A use import module array.Array as A
logic maxlen : int = 1000
type sparse_array 'a = {| val : array 'a; type sparse_array 'a = {| val : array 'a;
idx : array int; idx : array int;
back : array int; back : array int;
mutable card : int; mutable card : int;
default : 'a; |} default : 'a; |}
logic length (a: sparse_array 'a) : int = A.length a.val
logic is_elt (a: sparse_array 'a) (i: int) = logic is_elt (a: sparse_array 'a) (i: int) =
0 <= a.idx[i] < a.card and a.back[a.idx[i]] = i 0 <= a.idx[i] < a.card and a.back[a.idx[i]] = i
...@@ -42,18 +38,20 @@ back +-+-+-+-------------------+ ...@@ -42,18 +38,20 @@ back +-+-+-+-------------------+
else else
a.default a.default
logic sa_invariant (a: sparse_array 'a) = (* invariant *)
logic maxlen : int = 1000
logic length (a: sparse_array 'a) : int = A.length a.val
logic sa_inv (a: sparse_array 'a) =
0 <= a.card <= length a <= maxlen and 0 <= a.card <= length a <= maxlen and
A.length a.val = A.length a.idx = A.length a.back and A.length a.val = A.length a.idx = A.length a.back and
forall i : int. forall i : int.
0 <= i < a.card -> 0 <= i < a.card ->
0 <= a.back[i] < length a and a.idx[a.back[i]] = i 0 <= a.back[i] < length a and a.idx[a.back[i]] = i
lemma permutation : (* creation *)
forall a: sparse_array 'a. sa_invariant a ->
a.card = a.length ->
forall i: int. 0 <= i < a.length ->
0 <= a.idx[i] < a.length && a.back[a.idx[i]] = i
parameter malloc : n:int -> {} array 'a { A.length result = n } parameter malloc : n:int -> {} array 'a { A.length result = n }
...@@ -64,24 +62,33 @@ back +-+-+-+-------------------+ ...@@ -64,24 +62,33 @@ back +-+-+-+-------------------+
back = malloc sz; back = malloc sz;
card = 0; card = 0;
default = d |} default = d |}
{ sa_invariant result and result.card = 0 and { sa_inv result and result.card = 0 and
result.default = d and length result = sz } result.default = d and length result = sz }
(* access *)
let test (a: sparse_array 'a) i = let test (a: sparse_array 'a) i =
{ 0 <= i < length a and sa_invariant a } { 0 <= i < length a and sa_inv a }
0 <= a.idx[i] && a.idx[i] < a.card && a.back[a.idx[i]] = i 0 <= a.idx[i] && a.idx[i] < a.card && a.back[a.idx[i]] = i
{ result=True <-> is_elt a i } { result=True <-> is_elt a i }
let get (a: sparse_array 'a) i = let get (a: sparse_array 'a) i =
{ 0 <= i < length a and sa_invariant a } { 0 <= i < length a and sa_inv a }
if test a i then if test a i then
a.val[i] a.val[i]
else else
a.default a.default
{ result = value a i } { result = value a i }
(* assignment *)
lemma permutation :
forall a: sparse_array 'a. sa_inv a ->
a.card = a.length ->
forall i: int. 0 <= i < a.length -> is_elt a i
let set (a: sparse_array 'a) i v = let set (a: sparse_array 'a) i v =
{ 0 <= i < length a and sa_invariant a } { 0 <= i < length a and sa_inv a }
a.val[i] <- v; a.val[i] <- v;
if not (test a i) then begin if not (test a i) then begin
assert { a.card < length a }; assert { a.card < length a };
...@@ -89,7 +96,7 @@ back +-+-+-+-------------------+ ...@@ -89,7 +96,7 @@ back +-+-+-+-------------------+
a.back[a.card] <- i; a.back[a.card] <- i;
a.card <- a.card + 1 a.card <- a.card + 1
end end
{ sa_invariant a and { sa_inv a and
value a i = v and value a i = v and
forall j:int. j <> i -> value a j = value (old a) j } forall j:int. j <> i -> value a j = value (old a) j }
......
theory Test theory Bijection
use export int.Int
use import bool.Bool logic n : int
logic f int : int
type t 'a = {| a: 'a; b: bool; c: 'a |} axiom dom_f : forall i: int. 0 <= i < n -> 0 <= f i < n
logic g int : int
goal G: forall x: t bool. axiom gf : forall i: int. 0 <= i < n -> g (f i) = i
{| x with a = 0 |}.a = 0 end
theory Test1
logic id (i: int) : int = i
clone import Bijection with logic f = id, lemma dom_f
goal G: n > 4 -> g (id 4) = 4
end end
theory Order theory Order
...@@ -19,41 +23,6 @@ theory Order ...@@ -19,41 +23,6 @@ theory Order
axiom le_trans: forall x y z : t. x <= y -> y <= z -> x <= z axiom le_trans: forall x y z : t. x <= y -> y <= z -> x <= z
end end
theory List
type list 'a = Nil | Cons 'a (list 'a)
logic mem (x: 'a) (l: list 'a) = match l with
| Nil -> false
| Cons y r -> x = y \/ mem x r
end
end
theory SortedList
use import List
clone import Order as O
inductive sorted (l : list t) =
| sorted_nil :
sorted Nil
| sorted_one :
forall x:t. sorted (Cons x Nil)
| sorted_two :
forall x y : t, l : list t.
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
lemma sorted_Cons:
forall x: t, l: list t. sorted (Cons x l) ->
forall y: t. mem y l -> x <= y
end
theory SortedIntList
use import int.Int
use import List
clone import SortedList with type O.t = int, logic O.(<=) = (<=)
goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil)))
end
(* (*
Local Variables: Local Variables:
compile-command: "make -C .. tests/test-jcf.gui" compile-command: "make -C .. tests/test-jcf.gui"
......
module PoorArrays
use import int.Int
use import module ref.Ref
use import map.Map as M
type array_contents 'a = {| length: int; elts : map int 'a |}
type array 'a = ref (array_contents 'a)
parameter get (a: array 'a) (i: int) :
{ 0 <= i < length !a } 'a { result = M.get !a.elts i }
parameter set (a: array 'a) (i: int) (v: 'a) :
{ 0 <= i < length !a }
unit writes a
{ !a.length = !(old a).length and !a.elts = M.set !(old a).elts i v }
end
module M module M
use import int.Int use import int.Int
......
...@@ -82,15 +82,6 @@ theory OrderedUnitaryCommutativeRing ...@@ -82,15 +82,6 @@ theory OrderedUnitaryCommutativeRing
forall x y z : t. x <= y -> x + z <= y + z forall x y z : t. x <= y -> x + z <= y + z
axiom CompatOrderMult : axiom CompatOrderMult :
forall x y z : t. x <= y -> zero <= z -> x * z <= y * z forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
(*
lemma InvMult : forall x y : t. (-x) * y = - (x * y) = x * (-y)
lemma InvSquare : forall x : t. x * x = (-x) * (-x)
lemma ZeroMult : forall x : t. x * zero = zero = zero * x
lemma SquareNonNeg1 : forall x : t. x <= zero -> zero <= x * x
lemma SquareNonNeg : forall x : t. zero <= x * x
lemma ZeroLessOne : zero <= one
*)
end end
theory Field theory Field
...@@ -111,3 +102,16 @@ theory OrderedField ...@@ -111,3 +102,16 @@ theory OrderedField
axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
end end
(* to be discussed: should we add the following lemmas, and where
lemma InvMult : forall x y : t. (-x) * y = - (x * y) = x * (-y)
lemma InvSquare : forall x : t. x * x = (-x) * (-x)
lemma ZeroMult : forall x : t. x * zero = zero = zero * x
lemma SquareNonNeg1 : forall x : t. x <= zero -> zero <= x * x
lemma SquareNonNeg : forall x : t. zero <= x * x
lemma ZeroLessOne : zero <= one
*)
...@@ -13,7 +13,6 @@ theory Int ...@@ -13,7 +13,6 @@ theory Int
end end
theory Abs theory Abs
use import Int use import Int
......
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