see also the index (by topic, by tool, by reference, by year)
Inductive predicates
Examples involving a predicate defined inductively
- A Formal Proof of a Unix Path Resolution Algorithm
- A Formally Verified Interpreter for the Shell-like Language CoLiS
- A Formally Verified Symbolic Interpreter for a IMP language
- Edition distance
- Fibonacci sequence, linear algorithm, Java version
- In-Place Linked-List Reversal in Why3
- Program verification examples from the book "Software Foundations"
- Regular expression matching using residuals
- Selection Sort, C version
- Selection Sort, Java version
- Tree relabelling
- Variations on Semantics of Programming Languages
- WP revisited in Why3
see also the index (by topic, by tool, by reference, by year)