ring_buffer: Seq.get instead of Seq.([])

parent a85c6c98
prelude "(* This file is generated by Why3's coq-ssreflect driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
printer "coq"
filename "%t.v"
valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
transformation "eliminate_non_lambda_set_epsilon"
transformation "eliminate_projections"
transformation "simplify_formula"
theory BuiltIn
prelude "Require Import ssrwhy3."
syntax type int "int"
syntax type real "R"
syntax predicate (=) "(%1 = %2)"
end
theory Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
end
theory bool.Bool
syntax function andb "(Init.Datatypes.andb %1 %2)"
syntax function orb "(Init.Datatypes.orb %1 %2)"
syntax function xorb "(Init.Datatypes.xorb %1 %2)"
syntax function notb "(Init.Datatypes.negb %1)"
syntax function implb "(Init.Datatypes.implb %1 %2)"
end
theory map.Map
syntax type map "(%1 -> %2)%type"
syntax function get "(%1 %2)"
remove prop Const
end
theory int.Int
prelude "Require Import ssralg ssrnum.
Import GRing.Theory Num.Theory.
Local Open Scope ring_scope.
"
syntax function zero "0%Z"
syntax function one "1%Z"
syntax function (+) "(%1 + %2)%Z"
syntax function (-) "(%1 - %2)%Z"
syntax function ( * ) "(%1 * %2)%Z"
syntax function (-_) "(-%1)%Z"
syntax predicate (<=) "is_true (%1 <= %2)%Z"
syntax predicate (<) "is_true (%1 < %2)%Z"
syntax predicate (>=) "is_true (%1 >= %2)%Z"
syntax predicate (>) "is_true (%1 > %2)%Z"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop ZeroLessOne
end
......@@ -161,9 +161,9 @@ module RingBufferSeq
self.len = S.length self.sequence /\
forall i: int. 0 <= i < self.len ->
(self.first + i < size ->
S.([]) self.sequence i = self.data[self.first + i]) /\
S.get self.sequence i = self.data[self.first + i]) /\
(0 <= self.first + i - size ->
S.([]) self.sequence i = self.data[self.first + i - size])
S.get self.sequence i = self.data[self.first + i - size])
}
(* total capacity of the buffer *)
......@@ -204,14 +204,14 @@ module RingBufferSeq
let head (b: buffer 'a) : 'a
requires { length b > 0 }
ensures { result = S.([]) b.sequence 0 }
ensures { result = S.get b.sequence 0 }
= b.data[b.first]
let pop (b: buffer 'a) : 'a
requires { length b > 0 }
writes { b.first, b.len, b.sequence }
ensures { length b = (old (length b)) - 1 }
ensures { result = S.([]) (old b.sequence) 0 }
ensures { result = S.get (old b.sequence) 0 }
ensures { b.sequence = (old b.sequence)[1 ..] }
= ghost b.sequence <- b.sequence[1 ..];
let r = b.data[b.first] 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