search

informalsystems / vdd

Verification-Driven Development
21 stars 0 forks source link

TLA+ coding conventions #16

Open adizere opened 4 years ago

adizere commented 4 years ago

Summary

Problem: we don't have any conventions or standards on writing TLA+ code. A quick web search does not reveal any existing resource either.

We should try to define a minimal set of conventions & examples for helping us write TLA+ code consistently.

Motivation & description

@ancazamfir recently raised the issue of inconsistent coding style in our TLA+ specs. There's already quite a few of us writing TLA+. Among others, cc-ing here: @josef-widder @konnov @istoilkovska @milosevic @ancazamfir. Without a pre-existing standard in the community, and without a basic guideline among ourselves, it is inevitable that each of us will develop (or stick to) their own style. But this would not be productive, nor will it help us in writing quality code.

It would be useful to:

konnov commented 4 years ago

I think we can have some syntactic conventions, e.g., on naming variables, parameters, and operators. However, I would be very careful about imposing "coding" restrictions. The point of TLA+ specs is to write them as concise as possible and as much to the point as possible. It may be more like writing a paper: You can immediately tell apart a good paper from a bad one, but there is no rigid set of rules on how to write a good one.

konnov commented 4 years ago

Leslie Lamport once wrote a note on modules, where he warns not to overengineer the specs.

konnov commented 4 years ago

On the other hand, all of us start to collect "good practices". Maybe we should just create a markdown file, where everybody could add their tricks and explain, why these are good practices.

milosevic commented 4 years ago

Coding standards do not ensure code quality. I still find them useful as they normally increase reader friendliness :) As a reader you are less surprised. Good practices are something different, and as there are not many good resources on TLA+, i.e., how to properly use it to model some concepts, it seems very useful to collect good practices we discover.

adizere commented 4 years ago

Thanks, the note linked above is great read!

A markdown (or a few) would fit perfectly for what I have in mind. I think we want both standards+practices, and we can start with the former since they're simpler. To give a simple example of what we noticed can create some friction: try to agree on which of these is preferable.. or should we prefer one over another?

IsEven(x) == IF x % 2 = 0 
             THEN TRUE
             ELSE FALSE

or

IsEven(x) == IF x % 2 = 0 
                 THEN TRUE
                 ELSE FALSE

or

IsEven(x) == IF x % 2 = 0 THEN TRUE
             ELSE FALSE
konnov commented 4 years ago

I am still struggling with a good indentation practice in TLA+. My current style is like that:

IsEven(x) ==
  IF x % 2 = 0
  THEN TRUE
  ELSE FALSE

I think I know what you mean, but here is a pedantic note that shows semantically the best solution:

IsEven(x) == x % 2 = 0
ancazamfir commented 4 years ago

IsEven(x) == x % 2 = 0 Yes! that is true and should be mentioned.

or, for multi-line-blocks under IF/ ELSE

Foo(x) == 
    IF pred(x) THEN 
        ...
    ELSE 
        ...

Note that i like THEN in same line with IF, saves a line, reads better to me, it is close to programming languages. It doesn't have to be this way, but just to show that we have as many styles currently as people writing models. There are other questions:

Before we had automatic formatting tools, beautifiers, linters, etc., we had "coding standards". They were not only for formatting, variable naming conventions, but were also proposing general and domain specific good practices.

So yes, let's start an .md file and add to it slowly. I think it would help with having consistent specs.

adizere commented 4 years ago

As a long-term goal, it would be awesome to have something like go fmt (info). There is also work on a linter for TLA+.

@andrey-kuprianov :

... an idea came to me on writing a kind of an educational resource with pages like "How to express X in TLA+"... as good resources on TLA+ are so scarce... standards/conventions is another step in this direction. We also have the Linter idea on our Apalache roadmap: https://github.com/konnov/apalache/issues/120.

konnov commented 4 years ago

Pretty-printing TLA+ is far from being easy. Leslie Lamport once wrote a TLA+ spec on the indentation and formatting, so you can guess the complexity ;-)

shonfeder commented 4 years ago

Pretty-printing TLA+ is far from being easy. Leslie Lamport once wrote a TLA+ spec on the indentation and formatting, so you can guess the complexity ;-)

I found this googling around for that, lol:

The grammar of TLA+ is too complex to be described in BNF. There is a link to a TLA+ specification of the TLA+ grammar on https://groups.google.com/forum/#!topic/tlaplus/G1poTG5XK8E [the link is broken tho]

Maybe we need a nice, regular, well behaved, describable-in-BNF, surface syntax that compiles to TLA+:

(def Foo (x)
  (if (pred x)
     (...)
     (...)))

S-expressions ftw! :stuck_out_tongue_winking_eye:

jk, btw

konnov commented 3 years ago

Maybe we need a nice, regular, well behaved, describable-in-BNF, surface syntax that compiles to TLA+

@shonfeder , you made quite an awesome observation in May. It has been stuck in my head for a while. I think it is a very good idea. Essentially, our IR provides one with such a basic representation. We just have to write it with S-expressions. I am planning to fix the SANY-to-IR importer a bit and then expose the IR using the S-expressions. Although it is not very readable, it is still better than JSON.

arnaudbos commented 3 years ago

Hi, sorry to bother but since you're talking about S-expressions...

I'm starting to specify an algorithm and since its implementation will be in/for Clojure, I'll probably be using this library to write the spec. Just to... be consistent? have fun.
Maybe you've come across it before, maybe not. I thought that its salt.transpiler namespace may be of interest to you, considering the previous two comments.

Anyways, thanks a lot (❤️) for your work on this guide. It's a bit abstract to me at this point, especially regarding what section should contain what exactly or if it is applicable to every domain. But it's really nice to see people come up with a structure for writting specifications and since it's the first attempt (for lack of a better word) I've seen so far at doing this, I'll try to stick with it!

konnov commented 3 years ago

That's nice. Thank you for the pointer on salt! We also have a LISPy intermediate representation of TLA operators in Apalache. That seems to be quite a natural idea. We build our IR from TLA+ by running the SANY parser. So you might think about having this translation chain one day: TLA+ -> Apalache IR -> Salt.

If you are interested in coding practices, we have also started this PR on TLA+ idioms.

I also feel that TLA+ is lacking a good starting manual, especially on the "+" part. We will fix that!

konnov commented 3 years ago

Just a note on salt. As far as I can see from their code, they resolve non-determinism by randomization. Sure, this is the most pragmatic way to resolve non-determinism in a simulator. TLC and Apalache do an exhaustive analysis of possible non-deterministic choices.