Dafny toy

Deductively verifies a program using Hoare Logic & First Order Logic

Dafny engine

Self-Verifying Prgrogramming Language made by Microsoft Dafny

Basics

{Pre-cond} program {Post-cond} for loops: {Pre-cond} {Invariant} {Invariant and cond} loop {Invariant} {Invariant and not cond} {Post-cond}

Tips

• Specs are the most important things!! (without specs, impossible to verify)
• Invariant is hard to find, but use your intuition :)