some axiomatizations are now definitions

parent cb9aa0a2
......@@ -18,17 +18,15 @@ module McCarthy91
(* non-recursive implementation using a while loop *)
use import ref.Ref
use import int.Iter
function f (x: int) : int = if x <= 100 then 91 else x-10
(* iter k x = f^k(x) *)
clone import int.Iter with type t = int, function f = f
let f91_nonrec (n0: int) ensures { result = f n0 }
= let e = ref 1 in
let n = ref n0 in
while !e > 0 do
invariant { !e >= 0 /\ iter !e !n = f n0 }
invariant { !e >= 0 /\ iter f !e !n = f n0 }
variant { 101 - !n + 10 * !e, !e }
if !n > 100 then begin
n := !n - 10;
......
......@@ -32,6 +32,10 @@ module Mjrty
type candidate
val eq (x y: candidate) : bool
ensures { result <-> x = y }
(* FIXME: call it (=) when we have overloading *)
let mjrty (a: array candidate) : candidate
requires { 1 <= length a }
ensures { 2 * numof a result 0 (length a) > length a }
......@@ -47,7 +51,7 @@ module Mjrty
if !k = 0 then begin
cand := a[i];
k := 1
end else if !cand = a[i] then
end else if eq !cand a[i] then
incr k
else
decr k
......@@ -58,7 +62,7 @@ module Mjrty
k := 0;
for i = 0 to n-1 do
invariant { !k = numof a !cand 0 i /\ 2 * !k <= n }
if a[i] = !cand then begin
if eq a[i] !cand then begin
incr k;
if 2 * !k > n then raise Found
end
......
......@@ -393,27 +393,11 @@ theory Fact
use import Int
function fact int : int
axiom fact0: fact 0 = 1
axiom factn: forall n:int. n >= 1 -> fact n = n * fact (n-1)
(* in the new system it will be:
let rec function fact (n:int) : int =
let rec function fact (n: int) : int
requires { n >= 0 }
variant { n }
= if n = 0 then 1 else n * fact (n-1)
with the semantics
function fact int : int
axiom fact_def : \forall n:int [fact n].
n >= 0 -> fact n = if n = 0 then 1 else n * fact (n-1)
*)
end
(** {2 Generic iteration of a function} *)
......@@ -422,17 +406,15 @@ theory Iter
use import Int
type t
function f t : t
function iter int t : t
(** [iter k x] is [f^k(x)] *)
let rec function iter (f: 'a -> 'a) (k: int) (x: 'a) : 'a
requires { k >= 0 }
variant { k }
= if k = 0 then x else iter f (k - 1) (f x)
axiom iter_0: forall x: t. iter 0 x = x
axiom iter_s: forall k: int, x: t. 0 < k -> iter k x = iter (k-1) (f x)
lemma iter_1: forall f, x: 'a. iter f 1 x = f x
lemma iter_1: forall x: t. iter 1 x = f x
lemma iter_s2: forall k: int, x: t. 0 < k -> iter k x = f (iter (k-1) x)
lemma iter_s: forall f, k, x: 'a. 0 < k -> iter f k x = f (iter f (k - 1) x)
end
......@@ -523,10 +505,11 @@ theory Fibonacci "Fibonacci numbers"
use import Int
function fib int : int
axiom fib0: fib 0 = 0
axiom fib1: fib 1 = 1
axiom fibn: forall n:int. n >= 2 -> fib n = fib (n-1) + fib (n-2)
let rec function fib (n: int) : int
requires { n >= 0 }
variant { n }
= if n = 0 then 0 else
if n = 1 then 1 else
fib (n-1) + fib (n-2)
end
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