Commit d820bb87 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix typing of some more examples.

parent 2216e866
......@@ -13,7 +13,7 @@ module Elt
use export list.Permut
type elt
predicate le elt elt
val predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
clone export list.Sorted with type t = elt, predicate le = le,
goal Transitive.Trans
......
......@@ -14,7 +14,7 @@ module MergesortQueue
use import queue.Queue
type elt
predicate le elt elt
val predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
clone export list.Sorted with type t = elt, predicate le = le,
goal Transitive.Trans
......
......@@ -25,12 +25,12 @@ module OptimalReplay
use import ref.Refint
use import array.Array
(* parameters [N] and [f] are introduced as logic symbols *)
constant n: int
axiom n_nonneg: 0 < n
val constant n: int
ensures { 0 < result }
function f int: int
axiom f_prop: forall k: int. 0 < k < n -> 0 <= f k < k
val function f (k:int): int
requires { 0 < k < n }
ensures { 0 <= result < k}
(* path from 0 to i of distance d *)
inductive path int int =
......
......@@ -210,11 +210,10 @@ module FiniteNumberOfRegisters
use import Spec
use import DWP
(** we have k registers, namely 0,1,...,k-1 *)
constant k: int
(** we assume having at least two registers, otherwise we can't add *)
axiom at_least_two_registers: k >= 2
(** we have k registers, namely 0,1,...,k-1,
and there are at least two of them, otherwise we can't add *)
val constant k: int
ensures { 2 <= result }
(** [compile e r] returns a list of instructions that stores the value
of [e] in register [r], without modifying any register [r' < r]. *)
......@@ -250,14 +249,13 @@ module OptimalNumberOfRegisters
use import Spec
use import DWP
(** we have k registers, namely 0,1,...,k-1 *)
constant k: int
(** we assume having at least two registers, otherwise we can't add *)
axiom at_least_two_registers: k >= 2
(** we have k registers, namely 0,1,...,k-1,
and there are at least two of them, otherwise we can't add *)
val constant k: int
ensures { 2 <= result }
(** the minimal number of registers needed to evaluate e *)
function n (e: expr) : int =
let rec function n (e: expr) : int =
match e with
| Evar _ -> 1
| Eneg e -> n e
......
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