alternative spec. langs compiling to TLA+

[jhou...@gmail.com]

Greetings,

I am trying to find a precise definition of the TLA+ language. Motivation is to explore a more accessible front-end that do not remind of LaTex scripts. (I am aware of PlusCal.)

Does TLA+ have a formal definition that an alternative front-end can target?

Is there a fundamental reason (non apparent to newbs such as my self) that these spec. languages have their current embodiment?

Thank you.

[Stephan Merz]

Hello,

a full definition of the TLA+ specification language appears in part IV of Specifying Systems (http://research.microsoft.com/en-us/um/people/lamport/tla/book.html). But maybe that's not what you are looking for?

Best regards,
Stephan

> --
> 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[fl]

 

Is there a fundamental reason (non apparent to newbs such as my self) that these spec. languages have their current embodiment?

They are formal I guess. Principia Mathematica was already more challenging than a normal chat. But they are also more precise.

It has its virtue. You can't speak of what you can't define.

-- 

FL