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

[tlaplus] Re: (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)

From: Leslie Lamport <tlaplus.ll@xxxxxxxxx>
Date: Wed, 22 Apr 2020 10:42:36 -0700 (PDT)
References: <d54894f6-7282-4c29-be50-8cf19439953d@googlegroups.com>

I suspect there must be a way to break a spec like this into two parts, one is the spec for the algorithm, and the other is a scaffolding spec to contain all the auxiliary stuff needed to fully test the algorithm, much like the tests and test harness for production software.

You suspect correctly. The other part is a Toolbox model.

--
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/70e60428-0d37-4386-a262-dd317efd3260%40googlegroups.com.

References:
- [tlaplus] (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)
  - From: Todd Greenwood-Geer

Prev by Date: Re: [tlaplus] (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)
Next by Date: [tlaplus] learning tla+ strategy
Previous by thread: Re: [tlaplus] (NEWBIE) How to Limit the Scope or State Space? (auxillary/ghost variables)
Next by thread: [tlaplus] learning tla+ strategy
Index(es):
- Date
- Thread