|
SearchNavigationUser login |
literate programming with Alloy
|
||||
The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.
Theme originally designed by Chris Herberte
Actually, extra comma after field declaration is already legal for a very long time (I don't remember which release added it).
I added it specifically to make it easier to auto-generate models and also make Alloy models more robust against editing:
For example, the following is legal:
sig A {
x: Int ,
y: Int ,
}
The same uniformity also extends to function/predicate declarations.
For example, the following is legal:
pred isEqu [ a:Int , b:Int , ] { a = b }
Sincerely,
Felix Chang
Alloy4 Lead Developer
It seems that trailing commas are a syntactic nuisance.
Would the grammar become ambiguous if the trailing comma is made optional for every field declaration instead of just the last one?
i.e: would the following pose a problem for the compiler?
sig A {
x: Int
y: Int
}
Nicolas Rouquette
Flight Software Engineering & Architecture Group
Jet Propulsion Laboratory, Caltech, Pasadena, CA, USA
but I think the current system (of allowing extra comma) is good enough for auto code generators.
The Java programming language syntax also allows extra comma in its array declaration:
and the reason they gave was also because it would help auto code generators.
http://java.sun.com/docs/books/jls/third_edition/html/arrays.html
For humans, I think for maintainability, the current way is better, because it forces you to put at least one comma between 2 declaration.
I know I wouldn't like to read run-on models written by others, devoid of punctuation marks. :)
Sincerely,
Felix Chang
> devoid of punctuation marks. :)
A conjunction symbol (`and', `&&') can be replace by a newline; it seems reasonable that the declaration-comma (also a kind of conjunction) could be replaced by a newline, but perhaps only after a type.
Jeremy L. Jacob Tel: +44-1904-43-2747 Fax: +44-1904-43-2767
Jeremy.Jacob@cs.york.ac.uk http://www-users.cs.york.ac.uk/~jeremy/
Dept. of Computer Science, The University of York, YORK, YO10 5DD, UK
> it seems reasonable that the declaration-comma (also a kind of conjunction)
> could be replaced by a newline, but perhaps only after a type.
Ah, but you've actually touched a rather controversial feature: conjunction actually doesn't need newline.
Alloy3 and Alloy4 are not sensitive to newline or spaces, so the following are equivalent:
fact {
some x
some y
c => d
}
fact { some x some y c => d }
fact { (some x) && (some y) && (c => d) }
The parser is much, much trickier than it needed to be, specifically because I need to be able
to unambiguously determine when an expression ends *without* the help of any terminating punctuation.
This feature is retained for historical compatibility. Having done this for "conjunction of formula",
I certainly don't want to do this for "list of declarations" also.
:)
Sincerely,
Felix Chang
Alloy4 Lead Developer
That is horrible. You have my sympathies :-)
Jeremy L. Jacob Tel: +44-1904-43-2747 Fax: +44-1904-43-2767
Jeremy.Jacob@cs.york.ac.uk http://www-users.cs.york.ac.uk/~jeremy/
Dept. of Computer Science, The University of York, YORK, YO10 5DD, UK
> You have my sympathies
Thank you! Hence my previous comment about wanting to have at least one comma between two field declarations:
Felix wrote:
> For humans, I think for maintainability, the current way is better,
> because it forces you to put at least one comma between 2 declaration.
> I know I wouldn't like to read run-on models written by others, devoid of punctuation marks. :)
Note also that the curly brace syntax makes it easy to move groups of constraints around:
F
G
H
can be put inside a quantifier or let statement like this
all x: A {
F
G
H
}
Now of course Felix, as the implementer of the parser, naturally has a different opinion :-). I did concede on using square brackets for predicate and function invocations in A4, though; this makes parsing much easier, because with parens the characters "x (y)" can be parsed as a predicate call or as two formulas, with the second wrapped in parens. This seemed like a reasonable thing to do anyway, since we were able to use it to obtain greater syntactic uniformity between calls and joins (that is, you can write x.f instead of f[x] for both join and call).
Daniel