Safe Haskell | None |
---|---|

Language | Haskell2010 |

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

Example inductive proof to show partial correctness of the for-loop based fibonacci algorithm:

i = 0 k = 1 m = 0 while i < n: m, k = k, m + k i++

We do the proof against an axiomatized fibonacci implementation using an uninterpreted function.

# System state

System state. We simply have two components, parameterized over the type so we can put in both concrete and symbolic values.

## Instances

Queriable IO (S SInteger) (S Integer) Source # | Make our state queriable |

Show a => Show (S a) Source # | |

Generic (S a) Source # | |

Mergeable a => Mergeable (S a) Source # | |

type Rep (S a) Source # | |

Defined in Documentation.SBV.Examples.ProofTools.Fibonacci type Rep (S a) = D1 (MetaData "S" "Documentation.SBV.Examples.ProofTools.Fibonacci" "sbv-8.0-4OZZzEgTRNf59WYE3yYwTJ" False) (C1 (MetaCons "S" PrefixI True) ((S1 (MetaSel (Just "i") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "k") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)) :*: (S1 (MetaSel (Just "m") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a) :*: S1 (MetaSel (Just "n") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))) |

fibCorrect :: IO (InductionResult (S Integer)) Source #

Encoding partial correctness of the sum algorithm. We have:

`>>>`

Q.E.D.`fibCorrect`

NB. In my experiments, I found that this proof is quite fragile due to the use of quantifiers: If you make a mistake in your algorithm or the coding, z3 pretty much spins forever without finding a counter-example. However, with the correct coding, the proof is almost instantaneous!