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