[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Help understanding why this proof validates



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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUVYE8ZRF%3D8BNj8bDkU9fELtk1UNjVBfDYWC0ebhM8TkFA%40mail.gmail.com.