5 ms·
A while back I was exploring the use of 'soft' formal methods to help in evaluating correctness of some new modules we had to develop. I had come upon Alloy, wh
by kelvin0 10y ago
A while back I was exploring the use of 'soft' formal methods to help in evaluating correctness of some new modules we had to develop.
I had come upon Alloy, which seems like a gentler introduction to formal methods (Unlike Z or Coq).
http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/
Anyone have any experience using Alloy, or some other formal method?
- maramono 10y agoI've used it several times but the big problem with it is that once you have a nice, correct model that has been checked (and no counterexamples found), there's no way to translate it to code. This meand that your basically back on square one in terms of implementation. I really like (and use quite often) the ASM method instead. More of my thoughts here: http://ortask.com/how-i-designed-built-and-tested-a-temperature-logger-with-arduino-part-2/ http://ortask.com/how-i-designed-built-and-tested-a-temperat...
- nickpsecurity 10y agoThere's actually been imperative extensions and prolog compilers for it. Here you go: https://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf https://homes.cs.washington.edu/~emina/pubs/alloy.mscs13.pdf Also, for ASM's, the most interesting one I've seen is certified compiler project that is taking a lot less lines of code than CompCert: https://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf https://www.complang.tuwien.ac.at/andi/papers/hipeac14.pdf