A Why3 modelling of a token contract

handwritten-why3/token.mly is a handwritten Why3 input. This is prepared as a preliminary exploration before actually producing Why3 code from the Solidity compiler.

After installing why3, try

cd handwritten-why3
why3 ide token.mlw

After running some solvers, all goals should be green-ticked.

why3-by-solc will contain the sources. Not working yet.