How to prove RealInv' in the example "BubbleSort" ?

47 views
Skip to first unread message

cf Shi.

unread,
Jul 25, 2021, 11:00:43 PMJul 25
to tlaplus
Hello,
I'm new in tlaps and trying to finish the example BubbleSort.tla[1]. But the attempt was invalid
I have no idea on it, and whether I handled it in a disorderly way? How to prove RealInv' in the example "BubbleSort" ?

My approach to this is as follows: (of course, this is predictably not working)


<2>2. RealInv'
    <3>1. CASE pc = "Lbl_1"
       BY DEF TypeOK, RealInv, Lbl_1,
              Lbl_2, IsSortedTo,IsSorted,IsSortedFromTo, IsPermOf, Perms, **
    <3>2. CASE pc = "Lbl_2"
    <3>3. CASE pc = "Done"
        BY IsPermOfExchange DEF TypeOK, RealInv, Lbl_1, Lbl_2,IsSortedTo,
                 IsSorted,IsSortedFromTo, IsPermOf, Perms, **
    <3>4. QED
        BY <3>1,<3>2,<3>3 DEF TypeOK, RealInv, Lbl_1, Lbl_2 

-------------------------------------------------------------------------

[1] https://github.com/tlaplus/tlapm/blob/master/examples/BubbleSort.tla

Stephan Merz

unread,
Jul 26, 2021, 4:14:01 AMJul 26
to tla...@googlegroups.com
Hello,

that example is not an easy one for learning how to use the TLAPS proof assistant. I haven't tried to finish the proof, but I'll give you some hints on how to proceed.

The level-2 proof starts with

  <2> SUFFICES ASSUME Inv, Lbl_1 \/ Lbl_2 \* Next
               PROVE  Inv'

This indicates that the case distinction should be as follows:

    <3>1. CASE Lbl_1
    <3>2. CASE Lbl_2

Note that the actions such as Lbl_1 give you stronger hypotheses than just assuming, say, pc = "Lbl_1", which is but one conjunct of the definition of Lbl_1.

Indeed, we can then finish the proof by

    <3>. QED BY <3>1,<3>2 

Of course, the real work is in proving steps <3>1 and <3>2. I would not expect these proofs to work by brute force (BY expanding definitions and invoking utility lemmas), but probably you want to decompose them along the definitions of the actions. For Lbl_1, this suggests writing

      <4>1. CASE i < N
      <4>2. CASE ~(i < N)
      <4>. QED  BY <4>1, <4>2

For step <4>1, we can now gather information on the effect of the action:

        <5>1. /\ pc = "Lbl_1"
              /\ j' = i+1
              /\ pc' = "Lbl_2"
              /\ UNCHANGED << A, A0, i >>
          BY <3>1, <4>1 DEF Lbl_1

In particular, this tells us that we only need to worry about the conjunct of RealInv' that talks about what is expected when pc = Lbl_2. And now think about why the predicate holds true and guide the prover towards proving it. (As you observed, just adding all available facts and expanding all relevant definitions rarely works when proofs become a bit more complicated.) Steps <4>2 and <3>2 will be handled similarly. When the proof is done, you may be able to shorten it by compressing some proof steps into larger leaf proofs, but this is just cosmetics: I usually find that decomposing the proof helps me discover what is actually needed.

Note in particular that I used the case assumptions <3>1 and <4>1 in the proof of step <5>1: as a user you may find this unnecessary but TLAPS requires all necessary facts to be invoked explicitly.

Hope this helps (and if you finish the proof we'd love to add it to the collection of examples),

Stephan


--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ee395ae0-b749-4f4e-9da0-611f91564424n%40googlegroups.com.

cf Shi.

unread,
Jul 27, 2021, 5:21:17 AMJul 27
to tlaplus
Hi Stephan,
Thanks for your reply and help! I think that maybe I can  learn how to use the tlaps by other simple one firstly. It's very kind of you! Hope I will finish the proof soon.

Regards,
Shi

Karolis Petrauskas

unread,
Jul 27, 2021, 12:21:45 PMJul 27
to tla...@googlegroups.com
Tried to check this proof as well. But I'm getting the following error
when using tlapm from the updated_enabled_cdot branch.
As I understand, this branch is going to be the basis for the next
release, thus I hope this report will be useful.

(* created new ".tlacache/TLAPS.tlaps/TLAPS.thy" *)
(* fingerprints written in ".tlacache/TLAPS.tlaps/fingerprints" *)
File "/home/karolis/CODE/pub/tlapm/tmp/lib/tlaps/TLAPS.tla", line 1,
character 1 to line 362, character 77:
[INFO]: All 0 obligation proved.
tlapm ending abnormally with Invalid_argument("List.combine")
Raised at file "stdlib.ml", line 30, characters 20-45
Called from file "list.ml", line 263, characters 36-49
Called from file "e_levels.ml", line 228, characters 28-55
Called from file "e_levels.ml", line 234, characters 27-55
Called from file "e_levels.ml", line 413, characters 21-30
Called from file "e_levels.ml", line 934, characters 21-30
Called from file "e_levels.ml", line 992, characters 26-35
Called from file "e_visit.ml", line 222, characters 23-31
Called from file "e_visit.ml", line 223, characters 24-33
...
Called from file "e_visit.ml", line 223, characters 24-33
Called from file "e_visit.ml", line 146, characters 22-31
Called from file "e_levels.ml", line 560, characters 27-39
Called from file "prep.ml", line 1373, characters 12-42
Called from file "prep.ml", line 1458, characters 51-70
Called from file "camlinternalLazy.ml", line 29, characters 17-27
Re-raised at file "camlinternalLazy.ml", line 36, characters 4-11
Called from file "schedule.ml", line 83, characters 17-24
Called from file "schedule.ml", line 141, characters 37-62
Called from file "schedule.ml", line 181, characters 4-14
Called from file "tlapm.ml", line 208, characters 4-42
Called from file "tlapm.ml", line 408, characters 12-77
Called from file "tlapm.ml", line 503, characters 23-43
Called from file "list.ml", line 121, characters 24-34
Called from file "tlapm.ml", line 506, characters 13-40
Called from file "tlapm.ml", line 518, characters 8-33
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/84f326ac-a2f8-4966-a8c5-fa33a3d6c3c4n%40googlegroups.com.

Ioannis Filippidis

unread,
Sep 28, 2021, 8:48:54 PMSep 28
to tlaplus
Hi,

Thank you for reporting this issue, which was caused by a typo.
The correction has now been merged [1]. After this change,
`tlapm BubbleSort.tla` proves all proof obligations (in
the file `BubbleSort.tla` in the repository of `tlapm`).


Best regards,
Ioannis
Reply all
Reply to author
Forward
0 new messages