attempt to use Alt-Ergo's array theory (but kept in comments currently)

parent 9c5072d4
......@@ -115,6 +115,16 @@ theory algebra.AC
remove cloned prop Assoc.Assoc
end
(*
theory array.ArrayLength
syntax type t "%1 farray"
syntax logic select "(%1[%2])"
syntax logic store "(%1[%2 <- %3])"
remove prop Select_eq
remove prop Select_neq
end
*)
(*
Local Variables:
mode: why
......
......@@ -9,13 +9,13 @@
use array.Array as A
type table 'a 'b = A.t 'a (option 'b)
type table = A.t int (option int)
logic inv (t : table int int) =
logic inv (t : table) =
forall x y : int. A.select t x = Some y -> y = fib x
}
parameter table : ref (table int int)
parameter table : ref table
parameter add :
x:int -> y:int ->
......
......@@ -36,6 +36,7 @@ let ident_printer =
"false"; "forall"; "function"; "goal"; "if"; "int"; "bitv";
"logic"; "not"; "or"; "parameter"; "predicate";
"prop"; "real"; "then"; "true"; "type"; "unit"; "void";
"select"; "store";
]
in
let san = sanitizer char_to_alpha char_to_alnumus in
......
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