On Thursday, 31 July 2014 at 11:32:11 UTC, bearophile wrote:
A problem with code like this is that it's drowing in noise.
The precondition/invariant/variant code in the 't3' function is
obscuring what the code is actually doing on the data:
http://toccata.lri.fr/gallery/queens.en.html
Yes, if the algorithm is a bit involved it becomes complicated.
It is also expensive to get right, $100-$1000 per line of code?
However, simple stuff that you often have in a standard library
is usually easier on the eyes and easier to get right:
http://toccata.lri.fr/gallery/power.en.html
So, having a formally proven standard library would be quite
within reach. And if you also have inlining + assume() you could
do stuff like this
inline uint floor_sqrt(long x){
assert(x>=0);
uint r = _proven_floor_sqrt(x);
assume(r<=x*x);
assume( (r>(x-1)*(x-1)) || x==0 );
return r
}
Precompiled library:
uint _proven_floor_sqrt(long x){
assume(x>=0); // not test necessary, use this for optimization
return ...
}
Another nice thing is that you can replace _proven… with
handwritten machine language that has been exhaustively tested
(all combinations) and still let the compiler assume() the
postconditions with no runtime cost.
Another area where assume() is useful is for reading hardware
registers that are guaranteed to have certain values so no
runtime check is needed:
auto x = read_hw_register(123456);
assume( x==0 || x==1 || x==4 );
I have added a third version here:
http://rosettacode.org/wiki/Dutch_national_flag_problem#More_Verified_Version
Thanks, I like the way you go about this. Experimenting with the
syntax this way.
D lacks the pre-state (old a) and (at a 'Init), the loop
variants, the loop invariants (despite D has a invariant
keyword used for struct/classe invariants),
Yeah, I also think having invariant() in loops makes for more
readable code than assert/enforce.
I imagine that you could specify a reduced set of D and do this:
D-source => machinetranslate => prover-source
prover-source => prover => proof-source
proof-source + prover-source => machinetranslate => D-source
w/assume() etc
Btw, here is an example of an open source operating system kernel
vetted against a haskell modell of the kernel:
http://sel4.systems/
https://github.com/seL4/seL4/tree/master/haskell
So, this formal correctness support in one way or another is
clearly a valuable direction for a system level programming
language.
