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