3 ms·
This is indeed an interesting approach, but I wonder whether it also allows you to define 'implementations'. Let me explain. A lot of software development done
by fjfaase 3y ago
This is indeed an interesting approach, but I wonder whether it also allows you to define 'implementations'. Let me explain.
A lot of software development done is because computers are too slow for our demand.[1] It is nice to have an integer type 'nat' that can hold arbitrary large integer numbers (at least as large as fits in the memory model, I presume), but it is not very efficient to use it for every purpose. You also would like to have methods to verify that a certain implementation of a program using a certain 'limited' representation of integers, is correct.
[1] https://www.iwriteiam.nl/AoP.html https://www.iwriteiam.nl/AoP.html
- skydhash 3y agoYou may want to do a Find and Replace (piramid to pyramid).
- redjamjar 3y agoSo, you can use fixed-width data types in Dafny and verify properties about functions using them. For example, in our EVM implementation we have types like u8, u16, u256, etc. Of course, Dafny won't let operations on these types underflow or overflow, so it does mean more work ensuring your code doesn't allow this.