Floyd's examples from 'Assigning Meanings to Programs'

parent 3bba0f29
(* Program proofs from Floyd's "Assigning Meanings to Programs" (1967) *)
module Sum
(* computes the sum a[1] + ... + a[n] *)
use import int.Int
use import module ref.Ref
use import module array.Array
use import module array.ArraySum
let sum (a: array int) (n: int) =
{ 0 <= n < a.length }
let i = ref 1 in
let s = ref 0 in
while !i <= n do
invariant { 1 <= !i <= n+1 /\ !s = sum a 1 !i }
variant { n - !i }
s := !s + a[!i];
i := !i + 1
done;
!s
{ result = sum a 1 (n+1) }
end
module Division
(* Quotient and remainder of X div Y
Floyd's lexicographic variant is unnecessarily complex here, since
we do not seek for a variant which decreases at each statement, but
only at each execution of the loop body. *)
use import int.Int
use import module ref.Ref
let division (x: int) (y: int) =
{ 0 <= x /\ 0 < y }
let q = ref 0 in
let r = ref x in
while !r >= y do
invariant { 0 <= !r /\ x = !q * y + !r }
variant { !r }
r := !r - y;
q := !q + 1
done;
(!q, !r)
{ let q,r = result in 0 <= r < y /\ x = q * y + r }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/assigning_meanings_to_programs.gui"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/assigning_meanings_to_programs/why3session.xml">
<file name="../assigning_meanings_to_programs.mlw" verified="true" expanded="true">
<theory name="WP Sum" verified="true" expanded="true">
<goal name="WP_parameter sum" expl="correctness of parameter sum" sum="e400c1902a93c2db3f58b823d005001b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</theory>
<theory name="WP Division" verified="true" expanded="true">
<goal name="WP_parameter division" expl="correctness of parameter division" sum="c30339816d276e5cb31141054d5923e8" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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