Postcondition verification Complete
Static verification that ensure postconditions are derivable from evolve definitions
In this phase
- Expression grammar
- Exhaustiveness check
- Evolve totality check
- Guard consistency
- Error messages with positions
- Dead code detection
- Terminal state validation