Commit aa9b1886 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix invariant syntax in examples.

parent 2839e902
......@@ -41,10 +41,10 @@ module HashtblImpl
mutable data: array (list (key, 'a)); (* buckets *)
ghost mutable view: map key (option 'a); (* pure model *) }
invariant { 0 < length self.data }
invariant { 0 < length data }
invariant {
forall i: int. 0 <= i < length self.data -> good_hash self.data i }
invariant { forall k: key, v: 'a. good_data k v self.view self.data }
forall i: int. 0 <= i < length data -> good_hash data i }
invariant { forall k: key, v: 'a. good_data k v view data }
let create (n: int) : t 'a
requires { 1 <= n }
......
......@@ -20,12 +20,12 @@ module SimplePrioriyQueue
mutable h : int; (* index of the highest priority element, if any *)
ghost mutable bag: bag elt;
}
invariant { 0 <= self.size <= self.elems.length }
invariant { self.size = 0 \/ 0 <= self.h < self.size }
invariant { 0 <= size <= elems.length }
invariant { size = 0 \/ 0 <= h < size }
invariant { forall e: elt.
numof self.elems e 0 self.size = nb_occ e self.bag }
invariant { self.size > 0 -> forall e: elt. mem e self.bag ->
priority e <= priority self.elems[self.h] }
numof elems e 0 size = nb_occ e bag }
invariant { size > 0 -> forall e: elt. mem e bag ->
priority e <= priority elems[h] }
lemma numof_occ:
forall a: array elt, e: elt, l u: int.
......
......@@ -109,10 +109,10 @@ module LinearProbing
ghost mutable loc : map keym int; (* index where it is stored *)
}
(* at least one empty slot *)
invariant { 0 <= self.size < length self.data }
invariant { let n = Array.length self.data in
self.size + numofd self.data 0 n = n }
invariant { valid self.data self.view self.loc }
invariant { 0 <= size < length data }
invariant { let n = Array.length data in
size + numofd data 0 n = n }
invariant { valid data view loc }
let create (n: int) : t
requires { 0 < n }
......
......@@ -93,7 +93,7 @@ module BitsSpec
type t = {
ghost mdl: set int;
}
invariant { forall i. mem i self.mdl -> 0 <= i < size }
invariant { forall i. mem i mdl -> 0 <= i < size }
val empty () : t
ensures { is_empty result.mdl }
......@@ -146,7 +146,7 @@ module Bits "the 1-bits of an integer, as a set of integers"
ghost mdl: set int;
}
invariant {
forall i: int. (0 <= i < size /\ nth self.bv i) <-> mem i self.mdl
forall i: int. (0 <= i < size /\ nth bv i) <-> mem i mdl
}
let empty () : t
......
......@@ -150,7 +150,7 @@ module RAL
use import list.Nth
type t 'a = { r: ral 'a; ghost l: list 'a }
invariant { self.l = elements self.r }
invariant { l = elements r }
let empty () : t 'a
ensures { result.l = Nil }
......
......@@ -31,11 +31,11 @@ back +-+-+-+-------------------+
mutable card : int;
def : 'a; }
invariant {
0 <= self.card <= A.length self.values <= maxlen /\
A.length self.values = A.length self.index = A.length self.back /\
0 <= card <= A.length values <= maxlen /\
A.length values = A.length index = A.length back /\
forall i : int.
0 <= i < self.card ->
0 <= self.back[i] < A.length self.values /\ self.index[self.back[i]] = i
0 <= i < card ->
0 <= back[i] < A.length values /\ index[back[i]] = i
}
predicate is_elt (a: sparse_array 'a) (i: int) =
......
......@@ -60,7 +60,7 @@ module DancingLinks
(** we model the data structure with two arrays, nodes being
represented by array indices *)
type dll = { prev: array int; next: array int; ghost n: int }
invariant { length self.prev = length self.next = self.n }
invariant { length prev = length next = n }
(** node [i] is a valid node i.e. it has consistent neighbors *)
predicate valid_in (l: dll) (i: int) =
......
......@@ -339,9 +339,9 @@ type suffixArray = {
values : array int;
suffixes : array int;
}
invariant { self.values.length = self.suffixes.length /\
permutation self.suffixes.elts self.suffixes.length /\
SuffixSort.sorted self.values self.suffixes }
invariant { values.length = suffixes.length /\
permutation suffixes.elts suffixes.length /\
SuffixSort.sorted values suffixes }
let select (s:suffixArray) (i:int) : int
requires { 0 <= i < s.values.length }
......
......@@ -14,7 +14,7 @@ module AmortizedQueue
type queue 'a = { front: list 'a; lenf: int;
rear : list 'a; lenr: int; }
invariant { length self.front = self.lenf >= length self.rear = self.lenr }
invariant { length front = lenf >= length rear = lenr }
function sequence (q: queue 'a) : list 'a =
q.front ++ reverse q.rear
......
......@@ -22,15 +22,15 @@ module RingBuffer
ghost mutable sequence: list 'a;
}
invariant {
let size = Array.length self.data in
0 <= self.first < size /\
0 <= self.len <= size /\
self.len = L.length self.sequence /\
forall i: int. 0 <= i < self.len ->
(self.first + i < size ->
nth i self.sequence = Some self.data[self.first + i]) /\
(0 <= self.first + i - size ->
nth i self.sequence = Some self.data[self.first + i - size])
let size = Array.length data in
0 <= first < size /\
0 <= len <= size /\
len = L.length sequence /\
forall i: int. 0 <= i < len ->
(first + i < size ->
nth i sequence = Some data[first + i]) /\
(0 <= first + i - size ->
nth i sequence = Some data[first + i - size])
}
(* total capacity of the buffer *)
......@@ -155,15 +155,15 @@ module RingBufferSeq
ghost mutable sequence: S.seq 'a;
}
invariant {
let size = Array.length self.data in
0 <= self.first < size /\
0 <= self.len <= size /\
self.len = S.length self.sequence /\
forall i: int. 0 <= i < self.len ->
(self.first + i < size ->
S.get self.sequence i = self.data[self.first + i]) /\
(0 <= self.first + i - size ->
S.get self.sequence i = self.data[self.first + i - size])
let size = Array.length data in
0 <= first < size /\
0 <= len <= size /\
len = S.length sequence /\
forall i: int. 0 <= i < len ->
(first + i < size ->
S.get sequence i = data[first + i]) /\
(0 <= first + i - size ->
S.get sequence i = data[first + i - size])
}
(* total capacity of the buffer *)
......
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