content: -----------------------------------------------------------------------------
  -- |
  -- Module    : Documentation.SBV.Examples.ProofTools.Sum
  -- Copyright : (c) Levent Erkok
  -- License   : BSD3
  -- Maintainer: erkokl@gmail.com
  -- Stability : experimental
  --
  -- Example inductive proof to show partial correctness of the traditional
  -- for-loop sum algorithm:
  --
  -- @
  --     s = 0
  --     i = 0
  --     while i <= n:
  --        s += i
  --        i++
  -- @
  --
  -- We prove the loop invariant and establish partial correctness that
  -- @s@ is the sum of all numbers up to and including @n@ upon termination.
  -----------------------------------------------------------------------------
  
  {-# LANGUAGE DeriveTraversable     #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE NamedFieldPuns        #-}
  {-# LANGUAGE TypeFamilies          #-}
  
  {-# OPTIONS_GHC -Wall -Werror #-}
  
  module Documentation.SBV.Examples.ProofTools.Sum where
  
  import Data.SBV
  import Data.SBV.Tools.Induction
  
  -- * System state
  
  -- | System state. We simply have two components, parameterized
  -- over the type so we can put in both concrete and symbolic values.
  data S a = S { s :: a, i :: a, n :: a } deriving (Show, Traversable, Functor, Foldable)
  
  -- | 'Queriable instance for our state
  instance Queriable IO (S SInteger) where
    type QueryResult (S SInteger) = S Integer
    create = S <$> freshVar_ <*> freshVar_ <*> freshVar_
  
  -- | Encoding partial correctness of the sum algorithm. We have:
  --
  -- >>> sumCorrect
  -- Q.E.D.
  sumCorrect :: IO (InductionResult (S Integer))
  sumCorrect = induct chatty setup initial trans strengthenings inv goal
    where -- Set this to True for SBV to print steps as it proceeds
          -- through the inductive proof
          chatty :: Bool
          chatty = False
  
          -- This is where we would put solver options, typically via
          -- calls to 'Data.SBV.setOption'. We do not need any for this problem,
          -- so we simply do nothing.
          setup :: Symbolic ()
          setup = return ()
  
          -- Initially, @s@ and @i@ are both @0@. We also require @n@ to be at least @0@.
          initial :: S SInteger -> SBool
          initial S{s, i, n} = s .== 0 .&& i .== 0 .&& n .>= 0
  
          -- We code the algorithm almost literally in SBV notation:
          trans :: S SInteger -> S SInteger -> SBool
          trans S{s, i, n} S{s = s', i = i', n = n'} = (s', i', n') .== ite (i .<= n)
                                                                            (s+i, i+1, n)
                                                                            (s  , i  , n)
  
          -- No strengthenings needed for this problem!
          strengthenings :: [(String, S SInteger -> SBool)]
          strengthenings = []
  
          -- Loop invariant: @i@ remains at most @n+1@ and @s@ the sum of
          -- all the numbers up-to @i-1@.
          inv :: S SInteger -> SBool
          inv S{s, i, n} =    i .<= n+1
                          .&& s .== (i * (i - 1)) `sDiv` 2
  
          -- Final goal. When the termination condition holds, the sum is
          -- equal to all the numbers up to and including @n@. Note that
          -- SBV does not prove the termination condition; it simply is
          -- the indication that the loop has ended as specified by the user.
          goal :: S SInteger -> (SBool, SBool)
          goal S{s, i, n} = (i .== n+1, s .== (n * (n+1)) `sDiv` 2)
  