www.digitalmars.com         C & C++   DMDScript  

digitalmars.D.announce - Dependable Software by Design [sciam.com]

reply Lionello Lunesu <lio lunesu.remove.com> writes:
A must read:

http://www.sciam.com/article.cfm?articleID=00020D04-CFD8-146C-8D8D83414B7F0000&sc=I100322

The obvious question is: could some of the features of Alloy (the app 
mentioned in the article) be included in D / DMD?

L.
Sep 11 2006
parent reply Pragma <ericanderton yahoo.removeme.com> writes:
Lionello Lunesu wrote:

 A must read:
 
 http://www.sciam.com/article.cfm?articleID=00020D04-CFD8-146C-8D8D834
4B7F0000&sc=I100322 
 
 
 The obvious question is: could some of the features of Alloy (the app 
 mentioned in the article) be included in D / DMD?
 
 L.


This was news to me, so I went looking for the project mentioned in the 
article.  Why don't these news pieces ever link anything directly?

http://alloy.mit.edu/

Technically, D already has some of these features built in.  Namely, 
in/out/body and invariant sections provide a kind of contract checking 
that can be used to ensure correctness of a given model at runtime.

IMO:  I haven't groked the manual fully, but I'll go out on a limb and 
say that I think the Alloy language as such is a bad candidate for 
inclusion into D directly.  However it may prove useful for D in other 
ways...

Alloy it has significant overlap with D gramatically. I for one, would 
find it difficult to work in a language that contains sub-grammars that 
aren't orthogonal to the main one.  A practical example of this kind of 
language morass is working in ColdFusion Script (broken ECMAScript), 
Java and JavaScript in a web-app; the only way to keep from going 
cross-eyed here is to keep those languages as separate as possible.

Now, on the other hand: Alloy it has significant overlap with D 
*structurally*.  I can easily see Alloy being brought to task as a sort 
of "side-car" arrangement with D, but probably not in any official 
sense.  The D ABI provides enough leeway to do some neat things at 
runtime with any given program - and this may very well be enough for 
Alloy to function.  Another option would be to translate Alloy 
expressions into D, to provide modules suitable for linking in with a 
program, all bound together by an Alloy API.

-- 
- EricAnderton at yahoo
Sep 11 2006
parent Lionello Lunesu <lio lunesu.remove.com> writes:
Pragma wrote:

 Lionello Lunesu wrote:

 A must read:

 http://www.sciam.com/article.cfm?articleID=00020D04-CFD8-146C-8D8D834
4B7F0000&sc=I100322 


 The obvious question is: could some of the features of Alloy (the app 
 mentioned in the article) be included in D / DMD?

 L.


 
 This was news to me, so I went looking for the project mentioned in the 
 article.  Why don't these news pieces ever link anything directly?
 
 http://alloy.mit.edu/
 
 Technically, D already has some of these features built in.  Namely, 
 in/out/body and invariant sections provide a kind of contract checking 
 that can be used to ensure correctness of a given model at runtime.


Right. That's why a separate file with the assertions and contracts (the 
way Alloy does it) would not make sense. You'd be rewriting the 
contracts in a different grammar.

What I was thinking of was the part of Alloy that checks all contracts 
and comes up with a case that would fail. The SAT solver I think they 
called it.

In the printed version of sciam there's the example of a file system, 
with file and folder objects. They create a trivial file_move function: 
remove the file from it's current parent folder and add it to the new 
parent folder. One invariant is the fact that each file and folder must 
always be reachable from the root. It seems from this, Alloy can find 
the case where a folder is moved to itself. It would invalidate the 
invariant.

L.
Sep 11 2006