Dependable Software by Design [sciam.com]

[Lionello Lunesu]

Pragma wrote:
> Lionello Lunesu wrote:
>> 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.
> 
> 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.