Hello, I am writing a proof of a very simple PlusCal algorithm that iterates over a sequence and records its largest element. Currently I am just proving the type invariant, TypeOK:
---------------------------- MODULE FindHighest -----------------------------
EXTENDS Sequences, Naturals, Integers, TLAPS
(****************************************************************************
--algorithm Highest {
variables
f \in Seq(Nat);
h = -1;
i = 1;
define {
max(a, b) == IF a > b THEN a ELSE b
} {
lb: while (i <= Len(f)) {
h := max(h, f[i]);
i := i + 1;
}
}
}
****************************************************************************)
\* BEGIN TRANSLATION (chksum(pcal) = "c908a386" /\ chksum(tla) = "36657a9f")
VARIABLES f, h, i, pc
(* define statement *)
max(a, b) == IF a > b THEN a ELSE -2
vars == << f, h, i, pc >>
Init == (* Global variables *)
/\ f \in Seq(Nat)
/\ h = -1
/\ i = 1
/\ pc = "lb"
lb == /\ pc = "lb"
/\ IF i <= Len(f)
THEN /\ h' = max(h, f[i])
/\ i' = i + 1
/\ pc' = "lb"
ELSE /\ pc' = "Done"
/\ UNCHANGED << h, i >>
/\ f' = f
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars
Next == lb
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(pc = "Done")
\* END TRANSLATION
TypeOK ==
IF f = <<>>
THEN
/\ f = <<>>
/\ h = -1
/\ i = 1
ELSE
/\ f \in Seq(Nat)
/\ h \in Nat \cup {-1}
/\ i \in 1..Len(f)
THEOREM Spec => []TypeOK
PROOF
<1>a. Init => TypeOK
BY DEF Init, TypeOK
<1>b. TypeOK /\ UNCHANGED vars => TypeOK'
BY DEF TypeOK, vars
<1>c. TypeOK /\ Next => TypeOK'
<2> SUFFICES /\ TypeOK /\ lb => TypeOK'
/\ TypeOK /\ Terminating => TypeOK'
BY DEF Next
<2> QED
<1> QED BY PTL, <1>a, <1>b, <1>c DEF Spec
=============================================================================
Surprisingly, this proof checks out. I am using the 202210041448 1.5.0 pre-release of tlapm. I would assume the subproof of TypeOK /\ Next => TypeOK' would have to be greatly expanded in order to check properly. Also, doing simple modifications like changing the definition of max to:
max(a, b) == IF a > b THEN a ELSE -2
under which TypeOK should not hold results in tlapm still validating the proof:
tlapm FindHighest.tla
(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/home/ahelwer/.local/lib/tlaps/TLAPS.tla", line 1, character 1 to line 362
, character 77:
[INFO]: All 0 obligation proved.
fgrep: warning: fgrep is obsolescent; using grep -F
** Unexpanded symbols: ---
** Unexpanded symbols: ---
** Unexpanded symbols: ACTION_lb_, ACTION_Terminating_, STATE_TypeOK_
(* created new ".tlacache/FindHighest.tlaps/FindHighest.thy" *)
(* fingerprints written in ".tlacache/FindHighest.tlaps/fingerprints" *)
File "./FindHighest.tla", line 1, character 1 to line 79, character 77:
[INFO]: All 8 obligations proved.
Why is this proof validating? Am I accidentally typing something with SUFFICES that is interpreted as an OMITTED proof? Thanks,
Andrew Helwer
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
.