Timeline for What do we know about provably correct programs?
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 2, 2011 at 16:11 | comment | added | Radu GRIGore | Arbitrary properties can be encoded as fol assertions, in principle. I'm not sure what you want the tool to require. Do you want the specs to say what the output should be for all possible inputs? | |
| Jan 2, 2011 at 13:39 | comment | added | Alex ten Brink | As far as I understand Spec# (and its extension Sing#), it gives the programmer the ability to statically verify asserts, but it does not require the programmer does this, nor does it provide the ability to prove arbitrary properties of the code. | |
| Jan 2, 2011 at 9:45 | history | answered | Radu GRIGore | CC BY-SA 2.5 |