94 lines
2.6 KiB
Text
94 lines
2.6 KiB
Text
---- MODULE pc2_euclid ----
|
|
(* See https://en.wikipedia.org/wiki/Euclidean_algorithm for GCD *)
|
|
EXTENDS Naturals, TLC
|
|
|
|
CONSTANT N
|
|
|
|
(* Define the GCD operator *)
|
|
|
|
gcd(x, y) == CHOOSE i \in 1..x:
|
|
/\ x % i = 0
|
|
/\ y % i = 0
|
|
/\ \A j \in 1..x : /\ x % j = 0
|
|
/\ y % j = 0
|
|
=> i >= j
|
|
|
|
(*--algorithm EuclidAlg
|
|
(* Option -termination adds a WF_vars(Next) conjunct to the Spec *)
|
|
(* PlusCal options (-termination) *)
|
|
variables
|
|
u \in 2..N,
|
|
v \in 2..N,
|
|
u0 = u,
|
|
v0 = v;
|
|
begin
|
|
LBPrint:
|
|
print <<"init", u0, v0>>;
|
|
LBWhile:
|
|
while u /= 0 do
|
|
if u < v then u := v || v := u; \* The || means both assignments are done simultaneously
|
|
end if;
|
|
LBSubtract:
|
|
u := u - v
|
|
end while;
|
|
LBPrintResult:
|
|
print <<u0, v0, "have gcd", v>>;
|
|
assert v = gcd(u0, v0)
|
|
end algorithm*)
|
|
\* BEGIN TRANSLATION (chksum(pcal) = "bff004ee" /\ chksum(tla) = "e4ceb640")
|
|
VARIABLES pc, u, v, u0, v0
|
|
|
|
vars == << pc, u, v, u0, v0 >>
|
|
|
|
Init == (* Global variables *)
|
|
/\ u \in 2..N
|
|
/\ v \in 2..N
|
|
/\ u0 = u
|
|
/\ v0 = v
|
|
/\ pc = "LBPrint"
|
|
|
|
LBPrint == /\ pc = "LBPrint"
|
|
/\ PrintT(<<"init", u0, v0>>)
|
|
/\ pc' = "LBWhile"
|
|
/\ UNCHANGED << u, v, u0, v0 >>
|
|
|
|
LBWhile == /\ pc = "LBWhile"
|
|
/\ IF u /= 0
|
|
THEN /\ IF u < v
|
|
THEN /\ /\ u' = v
|
|
/\ v' = u
|
|
ELSE /\ TRUE
|
|
/\ UNCHANGED << u, v >>
|
|
/\ pc' = "LBSubtract"
|
|
ELSE /\ pc' = "LBPrintResult"
|
|
/\ UNCHANGED << u, v >>
|
|
/\ UNCHANGED << u0, v0 >>
|
|
|
|
LBSubtract == /\ pc = "LBSubtract"
|
|
/\ u' = u - v
|
|
/\ pc' = "LBWhile"
|
|
/\ UNCHANGED << v, u0, v0 >>
|
|
|
|
LBPrintResult == /\ pc = "LBPrintResult"
|
|
/\ PrintT(<<u0, v0, "have gcd", v>>)
|
|
/\ Assert(v = gcd(u0, v0),
|
|
"Failure of assertion at line 36, column 5.")
|
|
/\ pc' = "Done"
|
|
/\ UNCHANGED << u, v, u0, v0 >>
|
|
|
|
(* Allow infinite stuttering to prevent deadlock on termination. *)
|
|
Terminating == pc = "Done" /\ UNCHANGED vars
|
|
|
|
Next == LBPrint \/ LBWhile \/ LBSubtract \/ LBPrintResult
|
|
\/ Terminating
|
|
|
|
Spec == /\ Init /\ [][Next]_vars
|
|
/\ WF_vars(Next)
|
|
|
|
Termination == <>(pc = "Done")
|
|
|
|
\* END TRANSLATION
|
|
InOrder == u0 < v0
|
|
NotPrimePair == u /= 1 /\ v /= 1 \* Bad constraint: it will prevent some terminations.
|
|
Odds == u0 % 2 = 1 /\ v0 % 2 = 1
|
|
====
|