Alloy Community

User login

literate programming with Alloy

 
Posted on: Thu, 10/30/2008 - 10:10
nicolas.rouquette's picture
Joined: 2008-06-06
Points: 41
User is offline
literate programming with Alloy
latex & the noweb package (http://www.cs.tufts.edu/~nr/noweb/) could make for an attractive literate programming approach to interleaving descriptive text and chunks of an Alloy specification. Alloy syntax, despite being very concise and elegant, presents one inconvenience. Commas separate declarations in the body of a signature. If we want to interleave descriptions and declarations, we have to know for each declaration whether it is the last one in the body (i.e., no comma needed) or not (i.e., add a comma at the end).

Would making the comma optional add ambiguity to the language?

-- Nicolas.
 
Posted on: Thu, 10/30/2008 - 10:31    #1
Joined: 2008-05-15
Points: 334
User is offline
Hi:

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
 
Posted on: Tue, 11/11/2008 - 12:20    #2
nicolas.rouquette's picture
Joined: 2008-06-06
Points: 41
User is offline
Thanks Felix.

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
 
Posted on: Tue, 11/11/2008 - 16:33    #3
Joined: 2008-05-15
Points: 334
User is offline
Hi: I'll have to play with the grammar to see if it will work,
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
 
Posted on: Wed, 11/12/2008 - 04:34    #4
Joined: 2008-06-06
Points: 93
User is offline
> I know I wouldn't like to read run-on models written by others,
> 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
 
Posted on: Wed, 11/12/2008 - 06:59    #5
Joined: 2008-05-15
Points: 334
User is offline
> 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.

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
 
Posted on: Thu, 11/13/2008 - 03:24    #6
Joined: 2008-06-06
Points: 93
User is offline
> fact { some x some y c => d }

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
 
Posted on: Thu, 11/13/2008 - 07:38    #7
Joined: 2008-05-15
Points: 334
User is offline
Jeremy wrote:
> 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.  :)
 
Posted on: Wed, 02/25/2009 - 07:00    #8
dnj
dnj's picture
Joined: 2008-06-06
Points: 39
User is offline
I know I missed this comment when it was posted a few months ago, but I can't resist a response. From my perspective, this isn't a historical compatibility issue. I really wanted Alloy to (a) not be layout sensitive, and (b) not require end of line markers or conjunctions for multiple constraints. The rationale for (b) is that it makes it much easier to move constraints around if you don't have to take conjunctions with them, and by omitting end of line markers such as semicolons, we get an appearance that's more consistent with standard logic (and Z, incidentally). OK, I have to admit, I was also influenced by my favorite programming language, CLU, which managed to do without semicolons entirely...

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

Syndicate content  

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