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

Re: [tlaplus] C0 and TLAPLUS

I'm not sure what role you envision for C0 in combination to TLA

We might think of a sort of TLAPLUS0. We would use TLC and PLUSCAL.

No TLAPS, no temporal logic and no translation of the PLUSCAL  algorithm
into TLAPLUS macros.

The purpose would be to teach that expressing an algorithm using mathematical
concepts: relations, functions, set builder notation is more interesting than a
language to design an algorithm.

Then the transition of TLAPLUS0 to the rest of TLAPLUS would be easy.