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

Proving partial correctness of the SetGCD algorithm in the hyperbook

From: Jens Weber <jensh...@xxxxxxxxx>
Date: Thu, 23 Jun 2016 17:55:39 -0700 (PDT)

Hello TLA community,

I am trying to prove partial correctness of the SetGCD algorithm in the hyperbook - but I am not successful. Does anybody have a solution here? I am currently stuck on showing that S' is a finite set.

Thanks

Jens

Follow-Ups:
- Re: [tlaplus] Proving partial correctness of the SetGCD algorithm in the hyperbook
  - From: Stephan Merz

Prev by Date: [Dr. TLA+ Series] Paxos - Andrew Helwer (June 22nd, 10-11:30am PDT)
Next by Date: Re: [tlaplus] Proving partial correctness of the SetGCD algorithm in the hyperbook
Previous by thread: Re: [Dr. TLA+ Series] Paxos - Andrew Helwer (June 22nd, 10-11:30am PDT)
Next by thread: Re: [tlaplus] Proving partial correctness of the SetGCD algorithm in the hyperbook
Index(es):
- Date
- Thread