3 ms·
It's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in
by nickpsecurity 10y ago
It's more like SPARK Ada. It's a limited language designed for easy analysis by an automated prover. You can do preconditions, postconditions, and invariants in it. It was used in ExpressOS for mobile and I think IronClad Apps, too.
- bluejekyll 10y agoAre those pre and post conditions always executed? Or are they optional assertions that can be enabled/disabled?
- neilparikh 10y agoIf I'm reading the description correctly, the pre and post conditions are analyzed statically during compiling, and not added to the output code. So it's a similar idea to type checking, where the program won't even compile until the versifier is sure your code meets the conditions.