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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Fri, 14 Feb 2014 19:48:43 -0800 (PST)*References*: <8c5e643f-4706-400e-b836-16326060c6e2@googlegroups.com>

Thanks for spotting that. The "(pc = "Done") =>" should not be in the assertion. It will be corrected.

Leslie

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.

**References**:**position of PlusCal assert in Euclid from Hyperbook?***From:*Brian Beckman

- Prev by Date:
**position of PlusCal assert in Euclid from Hyperbook?** - Next by Date:
**Question on Inductive Invariants (page 44)?** - Previous by thread:
**position of PlusCal assert in Euclid from Hyperbook?** - Next by thread:
**Re: position of PlusCal assert in Euclid from Hyperbook?** - Index(es):