Commit 9ea6a417 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix some warnings and errors in examples.

parent 970eea5e
......@@ -203,6 +203,7 @@ goods examples/logic
goods examples
goods examples/foveoos11-cm
goods examples/hoare_logic
goods examples/avl "-L examples/avl"
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
goods examples/bitvectors "-L examples/bitvectors"
goods examples/in_progress
......
......@@ -84,7 +84,7 @@ module AVL
goal M.neutral
(** Abstract description of the data stored in the tree. *)
namespace D
scope D
type t 'a
(** Elements can be measured. *)
......
......@@ -48,7 +48,7 @@ end
module MonoidSumDef
use import list.List
namespace M
scope M
type t
constant zero : t
function op (a b:t) : t
......
......@@ -356,7 +356,7 @@ theory BV32
function size : int = 32
clone export BitVector with function size = size
clone export BitVector with function size, lemma size_positive
end
......@@ -365,7 +365,7 @@ theory BV64
function size : int = 64
clone export BitVector with function size = size
clone export BitVector with function size, lemma size_positive
end
......
......@@ -57,9 +57,9 @@ module SimpleQueue
mutable n: int;
ghost mutable contents: list 'a; (* data[m..n[ *)
}
invariant { 0 < length self.data }
invariant { 0 <= self.m <= self.n <= length self.data }
invariant { self.contents = to_list self.data self.m self.n }
invariant { 0 < length data }
invariant { 0 <= m <= n <= length data }
invariant { contents = to_list data m n }
let create (x: 'a) : t 'a
ensures { result.contents = Nil }
......
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