Commit 5998cb1b authored by Jean-Christophe's avatar Jean-Christophe

new examples from Dijkstra's papers 650 and 673

parent e9a542f8
(* EWD 650: A Theorem About Odd Powers of Odd Integers *)
module EWD673
use import int.Int
use import int.Power
use import number.Parity
use import number.Divisibility
use import module ref.Refint
let theorem (p: int) (k: int) (r: int) =
{ p >= 1 /\ odd p /\ k >= 1 /\ 1 <= r < power 2 k /\ odd r }
let x = ref 1 in
let d = ref 2 in
for i = 1 to k do
invariant
{ !d = power 2 i /\ 1 <= !x < !d /\
divides !d (power !x p - r) /\ odd !x }
if not (divides (2 * !d) (power !x p - r)) then x := !x + !d;
d := 2 * !d
done;
!x
{ 1 <= result < power 2 k /\
divides (power 2 k) (power result p - r) /\
odd result }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/ewd650.gui"
End:
*)
(* EWD 673: On Weak and Strong Termination *)
module EWD673
use import bool.Bool
use import int.Int
use import int.Lex2
use import module ref.Refint
val any_bool: unit -> {} bool {}
val any_nat: unit -> {} int { result >= 0 }
let s (x: ref int) (y: ref int) =
{ !x >= 0 /\ !y >= 0 }
while !x > 0 || !y > 0 do
invariant { !x >= 0 /\ !y >= 0 }
variant { (!x, !y) } with lex
if !x > 0 then begin decr x; y := any_nat () end;
(* else *)
if !y > 0 then decr y
done
{}
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/ewd673.gui"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/programs/ewd673/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="yices"
name="Yices"
version="1.0"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../ewd673.mlw"
verified="true"
expanded="true">
<theory
name="WP EWD673"
verified="true"
expanded="true">
<goal
name="WP_parameter s"
expl="parameter s"
sum="b5b0b1a69ec5abfed2f78edbdea29783"
proved="true"
expanded="true"
shape="iainfix >V3c0iainfix >V3c0iainfix >V6c0alexaTuple2V4V7aTuple2V3V2Aainfix >=V7c0Aainfix >=V4c0Iainfix =V7ainfix -V6c1FalexaTuple2V4V6aTuple2V3V2Aainfix >=V6c0Aainfix >=V4c0Iainfix =V6V5FIainfix >=V5c0FIainfix =V4ainfix -V3c1Fiainfix >V2c0alexaTuple2V3V8aTuple2V3V2Aainfix >=V8c0Aainfix >=V3c0Iainfix =V8ainfix -V2c1FalexaTuple2V3V2aTuple2V3V2Aainfix >=V2c0Aainfix >=V3c0iainfix >V3c0iainfix >V11c0alexaTuple2V9V12aTuple2V3V2Aainfix >=V12c0Aainfix >=V9c0Iainfix =V12ainfix -V11c1FalexaTuple2V9V11aTuple2V3V2Aainfix >=V11c0Aainfix >=V9c0Iainfix =V11V10FIainfix >=V10c0FIainfix =V9ainfix -V3c1Fiainfix >V2c0alexaTuple2V3V13aTuple2V3V2Aainfix >=V13c0Aainfix >=V3c0Iainfix =V13ainfix -V2c1FalexaTuple2V3V2aTuple2V3V2Aainfix >=V2c0Aainfix >=V3c0Iainfix >V2c0Iainfix >=V2c0Aainfix >=V3c0FFAainfix >=V0c0Aainfix >=V1c0Iainfix >=V0c0Aainfix >=V1c0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</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