Remix.run Logo
rramadass an hour ago

The first thing people need to study is the "Correct by Construction" approach to programming as espoused by Edsger Dijkstra. Only then will the mathematical concepts used in verification aware languages start making sense and one can better understand what and how to use it.

One of the best books to learn this from is The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - https://link.springer.com/book/10.1007/978-3-642-27919-5

The book actually uses Dijkstra's GCL language and wp-calculus along with Carroll Morgan's Refinement Calculus to demonstrate step-wise derivation of programs from specifications using a lot of examples.