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

Re: [tlaplus] Re: position of PlusCal assert in Euclid from Hyperbook?

right. I freshened my download and it does not have it any more.

On Sun, Feb 16, 2014 at 5:25 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:
I just checked the current version on the Web, dated 28 November 2013, and found that the instructions on page 39 did not contain (pc = "Done") in the assert statement it directed you to add.

On Friday, February 14, 2014 6:09:49 PM UTC-8, Brian Beckman wrote:
Following the instructions on page 39 of main.pdf, concerning an assert in Euclid's algorithm,
I find that the PlusCal translator, when processing this:

--algorithm Euclid
  {  variables x \in 1..N, y \in 1..N, x0 = x, y0 = y;
    { while (x /= y)
      { if (x < y) { y := y - x; }
        else       { x := x - y; }

      assert (pc = "Done") => (x = y) /\ (x = GCD(x0, y0));
  } }

produces (keeping only the relevant part)

ELSE /\ Assert((pc = "Done") => (x = y) /\ (x = GCD(x0, y0)),
               "Failure of assertion at line 16, column 7.")
     /\ pc' = "Done"
     /\ UNCHANGED << x, y >>

Notice the Assert is before the update of pc (via pc'). Doesn't this mean that the Assert never sees
(pc = "Done"), so its predicate is vapidly true, i.e., it doesn't actually check the stuff we want,
namely that (x=y)/\(x=GCD(x0,y0))?

I found this while following the instructions and attempting to change the consequent of
(pc = "Done")
to something false, and finding that TLA+ never produced an error.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/2WpNir-C1k4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.