proposed syntax changes

Coordinator
Aug 21, 2009 at 3:05 PM

I've posted a wikipage about proposed syntax changes to the annotation language. I understand this is a typical example of a bike shed problem and the discussion will last forever, but we definetely need to start it, as the current langauge gets really messy and is very counter-intuitive. Please post your comments and proposal here and/or on the wiki page.

With the proposed changes, it should be possible to run a (somewhat eleborate) perl script over the sources and get them adapted. I understand the most welcome changes are ditching spec/speconly distinction, special functions like set_closed_owns and introduction of a nice set syntax.

http://vcc.codeplex.com/Wiki/View.aspx?title=Proposed%20Syntax%20Changes

Thanks!

Michal

Coordinator
Aug 24, 2009 at 9:28 AM

Hi Michal,

  just a few comments / thoughts:

  • Set syntax: the current limitation of sets is that they are only pointer sets. "Typed" sets can be represented by (multi-dimensional) maps to bool. It would be good to have a nice syntax that works also for these maps, and maybe try to represent ptrset as such a map first (see issue 2264), to avoid duplicate work.
  • Usability: a major usability factor for the syntax is the ability to produce accurate source locations for the errors. Consider the difference between invariant(), which can deliver line-accurate errors, and inv_group(), which can't. We should aim for accurate message where possible (which becomes easier with less 'top-level' keywords). These accurate source locations often get broken, when users define derived macros (in particular taking multi-line arguments). We should take a look at common use cases, and maybe provide special syntax for these (e.g., spec functions with 'this' as an implicit argument or spec relations with and implicit this and old(current_state()) arguments).
  • Can you explain your motivation behind "use field/methods notation wherever possible"? I see a couple of pros / cons ("Doesn't look like C anymore", "Built-in stuff mostly distinguished from regular C", "Because users won't to be able to define derived functions, everything will be a big mix of regular functions and method notation", etc.)
  • The generics syntax is relatively ugly and currently requires separate macros from spec and speconly (see generic_instance in vcc.h and justspec in HV).
  • Can we break all of this down into digestible parts? For example, it might be good idea, to start with throwing out unused stuff (some more elements than listed on the wiki page qualify, I think)?
  • Do you know about more specific syntax criticism other than the ones listed above? "the current langauge gets really messy and is very counter-intuitive" is not really constructive :)

Thanks, Mark

Coordinator
Aug 24, 2009 at 11:54 AM
First, thanks for very constructive comments!

> Set syntax: the current limitation of sets is that they are only pointer sets. "Typed" sets can be represented by (multi-dimensional) maps to bool. It would be good to have a nice syntax that works also for these maps, and maybe try to represent ptrset as such a map first (see issue 2264), to avoid duplicate work.

You're right, we should have the set operators work on any map to bool.

> Usability: a major usability factor for the syntax is the ability to produce accurate source locations for the errors. Consider the difference between invariant(), which can deliver line-accurate errors, and inv_group(), which can't. We should aim for accurate message where possible (which becomes easier with less 'top-level' keywords). These accurate source locations often get broken, when users define derived macros (in particular taking multi-line arguments). We should take a look at common use cases, and maybe provide special syntax for these (e.g., spec functions with 'this' as an implicit argument or spec relations with and implicit this and old(current_state()) arguments).

Right. We may just want to re-implement the #define feature of C preprocessor within VCC, to keep the location information. Possibly with some VCC-specific enhancements (like implicit state).

> Can you explain your motivation behind "use field/methods notation wherever possible"? I see a couple of pros / cons (

For example, ->owner is a field, so is ->ref_cnt and so on. Some of them you can even assign. So the field notation makes sense from that perspective.

Using field syntax does not pollute the C namespace. We will make the VCC compiler recognize them in field position, and complain when there is already such a field defined (in which case you will need to use o->\owner, o->@owner or something like that to access the spec field, and keep using o->owner for the regular thing).

> "Doesn't look like C anymore",

The field notation does look like C. The methods not so much, but they are legal C (function pointer stored in a field). Arguably, forall(int x; ...) looks much more scary than o->open().

> "Built-in stuff mostly distinguished from regular C", "Because users won't to be able to define derived functions, everything will be a big mix of regular functions and method notation", etc.)

The user-defined stuff looks different seems like an disadvantage though. We were thinking of introducing an C#-like extension method syntax for defining those internally, I guess it could be also available for users.

> The generics syntax is relatively ugly and currently requires separate macros from spec and speconly (see generic_instance in vcc.h and justspec in HV).

I didn’t think about those yet, not much experience.

> Can we break all of this down into digestible parts? For example, it might be good idea, to start with throwing out unused stuff (some more elements than listed on the wiki page qualify, I think)?

Throwing stuff out, OK. But the switch to field-like notation, if we decide to do it, I think we need to do at once.

> Do you know about more specific syntax criticism other than the ones listed above? "the current langauge gets really messy and is very counter-intuitive" is not really constructive :)

True. What I don't like is that we pollute the C namespace more and more with our macros. This is not a problem for HV, because we have the entire codebase around, but will be a problem in future, should anyone else use VCC. The field thing gets rid of most of that problem, and vcc(...) makes it easier to deal with VCC function names clashing with user function names. I guess we could require the user functions shadowed by VCC functions to be quoted in vcc(...) blocks, or maybe for consistency with fields, the other way around.

We would also not relay on the preprocessor much anymore, so the error locations/messages would be more accurate.

The field notation should be also easier to explain (think tutorial). At least Ernie and Wolfram thought so.

Michal
Aug 25, 2009 at 12:21 PM

also the new notations reduce the number of parantheses which imho increases readability and at least partly eases the pain of VS lacking some proper bracket highlighting ;)

As you are cleaning up set notation why not also introduce some nice syntax (and semantics) for bit strings and operations like selecting bits/strings from a number/string, rotating bit strings, creating parametrized bit strings, concatenation etc. ?

I would need that for verifying low level/assembly code and its quite ugly to define this stuff in C using macros. In the end you are also not proving much other than "this obscure C expression equals some other obscure C expression". Not talking about there are in fact several possible implementations for such operations, which may differ in there efficiency on the prover.

So maybe once you are playing around with syntax/notation you might also consider this issue. I guess others' work would also profit from it.