-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.WeakestPreconditions.Append
-- Copyright : Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proof of correctness of an imperative list-append algorithm, using weakest
-- preconditions. Illustrates the use of SBV's symbolic lists together with
-- the WP algorithm.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE DeriveTraversable     #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE OverloadedLists       #-}
{-# LANGUAGE TypeFamilies          #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.WeakestPreconditions.Append where

import Data.SBV
import Data.SBV.Tools.WeakestPreconditions

import Prelude hiding ((++))
import qualified Prelude as P

import           Data.SBV.List ((++))
import qualified Data.SBV.List as L

import GHC.Generics (Generic)

-- * Program state

-- | The state of the length program, paramaterized over the element type @a@
data AppS a = AppS { forall a. AppS a -> a
xs :: a  -- ^ The first input list
                   , forall a. AppS a -> a
ys :: a  -- ^ The second input list
                   , forall a. AppS a -> a
ts :: a  -- ^ Temporary variable
                   , forall a. AppS a -> a
zs :: a  -- ^ Output
                   }
                   deriving ((forall x. AppS a -> Rep (AppS a) x)
-> (forall x. Rep (AppS a) x -> AppS a) -> Generic (AppS a)
forall x. Rep (AppS a) x -> AppS a
forall x. AppS a -> Rep (AppS a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (AppS a) x -> AppS a
forall a x. AppS a -> Rep (AppS a) x
$cfrom :: forall a x. AppS a -> Rep (AppS a) x
from :: forall x. AppS a -> Rep (AppS a) x
$cto :: forall a x. Rep (AppS a) x -> AppS a
to :: forall x. Rep (AppS a) x -> AppS a
Generic, Bool -> SBool -> AppS a -> AppS a -> AppS a
(Bool -> SBool -> AppS a -> AppS a -> AppS a)
-> (forall b.
    (Ord b, SymVal b, Num b, Num (SBV b)) =>
    [AppS a] -> AppS a -> SBV b -> AppS a)
-> Mergeable (AppS a)
forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[AppS a] -> AppS a -> SBV b -> AppS a
forall a.
Mergeable a =>
Bool -> SBool -> AppS a -> AppS a -> AppS a
forall a b.
(Mergeable a, Ord b, SymVal b, Num b, Num (SBV b)) =>
[AppS a] -> AppS a -> SBV b -> AppS a
forall a.
(Bool -> SBool -> a -> a -> a)
-> (forall b.
    (Ord b, SymVal b, Num b, Num (SBV b)) =>
    [a] -> a -> SBV b -> a)
-> Mergeable a
$csymbolicMerge :: forall a.
Mergeable a =>
Bool -> SBool -> AppS a -> AppS a -> AppS a
symbolicMerge :: Bool -> SBool -> AppS a -> AppS a -> AppS a
$cselect :: forall a b.
(Mergeable a, Ord b, SymVal b, Num b, Num (SBV b)) =>
[AppS a] -> AppS a -> SBV b -> AppS a
select :: forall b.
(Ord b, SymVal b, Num b, Num (SBV b)) =>
[AppS a] -> AppS a -> SBV b -> AppS a
Mergeable, Functor AppS
Foldable AppS
(Functor AppS, Foldable AppS) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> AppS a -> f (AppS b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    AppS (f a) -> f (AppS a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> AppS a -> m (AppS b))
-> (forall (m :: * -> *) a. Monad m => AppS (m a) -> m (AppS a))
-> Traversable AppS
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => AppS (m a) -> m (AppS a)
forall (f :: * -> *) a. Applicative f => AppS (f a) -> f (AppS a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AppS a -> m (AppS b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AppS a -> f (AppS b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AppS a -> f (AppS b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> AppS a -> f (AppS b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => AppS (f a) -> f (AppS a)
sequenceA :: forall (f :: * -> *) a. Applicative f => AppS (f a) -> f (AppS a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AppS a -> m (AppS b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> AppS a -> m (AppS b)
$csequence :: forall (m :: * -> *) a. Monad m => AppS (m a) -> m (AppS a)
sequence :: forall (m :: * -> *) a. Monad m => AppS (m a) -> m (AppS a)
Traversable, (forall a b. (a -> b) -> AppS a -> AppS b)
-> (forall a b. a -> AppS b -> AppS a) -> Functor AppS
forall a b. a -> AppS b -> AppS a
forall a b. (a -> b) -> AppS a -> AppS b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> AppS a -> AppS b
fmap :: forall a b. (a -> b) -> AppS a -> AppS b
$c<$ :: forall a b. a -> AppS b -> AppS a
<$ :: forall a b. a -> AppS b -> AppS a
Functor, (forall m. Monoid m => AppS m -> m)
-> (forall m a. Monoid m => (a -> m) -> AppS a -> m)
-> (forall m a. Monoid m => (a -> m) -> AppS a -> m)
-> (forall a b. (a -> b -> b) -> b -> AppS a -> b)
-> (forall a b. (a -> b -> b) -> b -> AppS a -> b)
-> (forall b a. (b -> a -> b) -> b -> AppS a -> b)
-> (forall b a. (b -> a -> b) -> b -> AppS a -> b)
-> (forall a. (a -> a -> a) -> AppS a -> a)
-> (forall a. (a -> a -> a) -> AppS a -> a)
-> (forall a. AppS a -> [a])
-> (forall a. AppS a -> Bool)
-> (forall a. AppS a -> Int)
-> (forall a. Eq a => a -> AppS a -> Bool)
-> (forall a. Ord a => AppS a -> a)
-> (forall a. Ord a => AppS a -> a)
-> (forall a. Num a => AppS a -> a)
-> (forall a. Num a => AppS a -> a)
-> Foldable AppS
forall a. Eq a => a -> AppS a -> Bool
forall a. Num a => AppS a -> a
forall a. Ord a => AppS a -> a
forall m. Monoid m => AppS m -> m
forall a. AppS a -> Bool
forall a. AppS a -> Int
forall a. AppS a -> [a]
forall a. (a -> a -> a) -> AppS a -> a
forall m a. Monoid m => (a -> m) -> AppS a -> m
forall b a. (b -> a -> b) -> b -> AppS a -> b
forall a b. (a -> b -> b) -> b -> AppS a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => AppS m -> m
fold :: forall m. Monoid m => AppS m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> AppS a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> AppS a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> AppS a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> AppS a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> AppS a -> b
foldr :: forall a b. (a -> b -> b) -> b -> AppS a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> AppS a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> AppS a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> AppS a -> b
foldl :: forall b a. (b -> a -> b) -> b -> AppS a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> AppS a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> AppS a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> AppS a -> a
foldr1 :: forall a. (a -> a -> a) -> AppS a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> AppS a -> a
foldl1 :: forall a. (a -> a -> a) -> AppS a -> a
$ctoList :: forall a. AppS a -> [a]
toList :: forall a. AppS a -> [a]
$cnull :: forall a. AppS a -> Bool
null :: forall a. AppS a -> Bool
$clength :: forall a. AppS a -> Int
length :: forall a. AppS a -> Int
$celem :: forall a. Eq a => a -> AppS a -> Bool
elem :: forall a. Eq a => a -> AppS a -> Bool
$cmaximum :: forall a. Ord a => AppS a -> a
maximum :: forall a. Ord a => AppS a -> a
$cminimum :: forall a. Ord a => AppS a -> a
minimum :: forall a. Ord a => AppS a -> a
$csum :: forall a. Num a => AppS a -> a
sum :: forall a. Num a => AppS a -> a
$cproduct :: forall a. Num a => AppS a -> a
product :: forall a. Num a => AppS a -> a
Foldable)

-- | Show instance, a bit more prettier than what would be derived:
instance Show (f a) => Show (AppS (f a)) where
  show :: AppS (f a) -> String
show AppS{f a
xs :: forall a. AppS a -> a
xs :: f a
xs, f a
ys :: forall a. AppS a -> a
ys :: f a
ys, f a
ts :: forall a. AppS a -> a
ts :: f a
ts, f a
zs :: forall a. AppS a -> a
zs :: f a
zs} = String
"{xs = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ f a -> String
forall a. Show a => a -> String
show f a
xs String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", ys = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ f a -> String
forall a. Show a => a -> String
show f a
ys String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", ts = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ f a -> String
forall a. Show a => a -> String
show f a
ts String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
", zs = " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ f a -> String
forall a. Show a => a -> String
show f a
zs String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
"}"

-- | 'Queriable' instance for the program state
instance Queriable IO (AppS (SList Integer)) where
  type QueryResult (AppS (SList Integer)) = AppS [Integer]
  create :: QueryT IO A
create = SList Integer
-> SList Integer -> SList Integer -> SList Integer -> A
forall a. a -> a -> a -> a -> AppS a
AppS (SList Integer
 -> SList Integer -> SList Integer -> SList Integer -> A)
-> QueryT IO (SList Integer)
-> QueryT IO (SList Integer -> SList Integer -> SList Integer -> A)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT IO (SList Integer)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_  QueryT IO (SList Integer -> SList Integer -> SList Integer -> A)
-> QueryT IO (SList Integer)
-> QueryT IO (SList Integer -> SList Integer -> A)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO (SList Integer)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_  QueryT IO (SList Integer -> SList Integer -> A)
-> QueryT IO (SList Integer) -> QueryT IO (SList Integer -> A)
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO (SList Integer)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_  QueryT IO (SList Integer -> A)
-> QueryT IO (SList Integer) -> QueryT IO A
forall a b. QueryT IO (a -> b) -> QueryT IO a -> QueryT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> QueryT IO (SList Integer)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_

-- | Helper type synonym
type A = AppS (SList Integer)

-- * The algorithm

-- | The imperative append algorithm:
--
-- @
--    zs = []
--    ts = xs
--    while not (null ts)
--      zs = zs ++ [head ts]
--      ts = tail ts
--    ts = ys
--    while not (null ts)
--      zs = zs ++ [head ts]
--      ts = tail ts
-- @
algorithm :: Stmt A
algorithm :: Stmt A
algorithm = [Stmt A] -> Stmt A
forall st. [Stmt st] -> Stmt st
Seq [ (A -> A) -> Stmt A
forall st. (st -> st) -> Stmt st
Assign ((A -> A) -> Stmt A) -> (A -> A) -> Stmt A
forall a b. (a -> b) -> a -> b
$ \A
st          -> A
st{zs = []}
                , (A -> A) -> Stmt A
forall st. (st -> st) -> Stmt st
Assign ((A -> A) -> Stmt A) -> (A -> A) -> Stmt A
forall a b. (a -> b) -> a -> b
$ \st :: A
st@AppS{SList Integer
xs :: forall a. AppS a -> a
xs :: SList Integer
xs} -> A
st{ts = xs}
                , String -> Invariant A -> Stmt A
forall {a}.
SymVal a =>
String -> Invariant (AppS (SList a)) -> Stmt (AppS (SList a))
loop String
"xs" (\AppS{SList Integer
xs :: forall a. AppS a -> a
xs :: SList Integer
xs, SList Integer
zs :: forall a. AppS a -> a
zs :: SList Integer
zs, SList Integer
ts :: forall a. AppS a -> a
ts :: SList Integer
ts} -> SList Integer
xs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
zs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ts)
                , (A -> A) -> Stmt A
forall st. (st -> st) -> Stmt st
Assign ((A -> A) -> Stmt A) -> (A -> A) -> Stmt A
forall a b. (a -> b) -> a -> b
$ \st :: A
st@AppS{SList Integer
ys :: forall a. AppS a -> a
ys :: SList Integer
ys} -> A
st{ts = ys}
                , String -> Invariant A -> Stmt A
forall {a}.
SymVal a =>
String -> Invariant (AppS (SList a)) -> Stmt (AppS (SList a))
loop String
"ys" (\AppS{SList Integer
xs :: forall a. AppS a -> a
xs :: SList Integer
xs, SList Integer
ys :: forall a. AppS a -> a
ys :: SList Integer
ys, SList Integer
zs :: forall a. AppS a -> a
zs :: SList Integer
zs, SList Integer
ts :: forall a. AppS a -> a
ts :: SList Integer
ts} -> SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
zs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ts)
                ]
  where loop :: String -> Invariant (AppS (SList a)) -> Stmt (AppS (SList a))
loop String
w Invariant (AppS (SList a))
inv = String
-> Invariant (AppS (SList a))
-> Maybe (Measure (AppS (SList a)))
-> Invariant (AppS (SList a))
-> Stmt (AppS (SList a))
-> Stmt (AppS (SList a))
forall st.
String
-> Invariant st
-> Maybe (Measure st)
-> Invariant st
-> Stmt st
-> Stmt st
While (String
"walk over " String -> ShowS
forall a. [a] -> [a] -> [a]
P.++ String
w)
                           Invariant (AppS (SList a))
inv
                           (Measure (AppS (SList a)) -> Maybe (Measure (AppS (SList a)))
forall a. a -> Maybe a
Just (\AppS{SList a
ts :: forall a. AppS a -> a
ts :: SList a
ts} -> [SList a -> SInteger
forall a. SymVal a => SList a -> SInteger
L.length SList a
ts]))
                           (\AppS{SList a
ts :: forall a. AppS a -> a
ts :: SList a
ts} -> SBool -> SBool
sNot (SList a -> SBool
forall a. SymVal a => SList a -> SBool
L.null SList a
ts))
                           (Stmt (AppS (SList a)) -> Stmt (AppS (SList a)))
-> Stmt (AppS (SList a)) -> Stmt (AppS (SList a))
forall a b. (a -> b) -> a -> b
$ [Stmt (AppS (SList a))] -> Stmt (AppS (SList a))
forall st. [Stmt st] -> Stmt st
Seq [ (AppS (SList a) -> AppS (SList a)) -> Stmt (AppS (SList a))
forall st. (st -> st) -> Stmt st
Assign ((AppS (SList a) -> AppS (SList a)) -> Stmt (AppS (SList a)))
-> (AppS (SList a) -> AppS (SList a)) -> Stmt (AppS (SList a))
forall a b. (a -> b) -> a -> b
$ \st :: AppS (SList a)
st@AppS{SList a
ts :: forall a. AppS a -> a
ts :: SList a
ts, SList a
zs :: forall a. AppS a -> a
zs :: SList a
zs} -> AppS (SList a)
st{zs = zs `L.snoc` L.head ts}
                                 , (AppS (SList a) -> AppS (SList a)) -> Stmt (AppS (SList a))
forall st. (st -> st) -> Stmt st
Assign ((AppS (SList a) -> AppS (SList a)) -> Stmt (AppS (SList a)))
-> (AppS (SList a) -> AppS (SList a)) -> Stmt (AppS (SList a))
forall a b. (a -> b) -> a -> b
$ \st :: AppS (SList a)
st@AppS{SList a
ts :: forall a. AppS a -> a
ts :: SList a
ts}     -> AppS (SList a)
st{ts = L.tail ts            }
                                 ]

-- | A program is the algorithm, together with its pre- and post-conditions.
imperativeAppend :: Program A
imperativeAppend :: Program A
imperativeAppend = Program { setup :: Symbolic ()
setup         = () -> Symbolic ()
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                           , precondition :: Invariant A
precondition  = SBool -> Invariant A
forall a b. a -> b -> a
const SBool
sTrue  -- no precondition
                           , program :: Stmt A
program       = Stmt A
algorithm
                           , postcondition :: Invariant A
postcondition = Invariant A
postcondition
                           , stability :: Stable A
stability     = Stable A
noChange
                           }
  where -- We must append properly!
        postcondition :: A -> SBool
        postcondition :: Invariant A
postcondition AppS{SList Integer
xs :: forall a. AppS a -> a
xs :: SList Integer
xs, SList Integer
ys :: forall a. AppS a -> a
ys :: SList Integer
ys, SList Integer
zs :: forall a. AppS a -> a
zs :: SList Integer
zs} = SList Integer
zs SList Integer -> SList Integer -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SList Integer
xs SList Integer -> SList Integer -> SList Integer
forall a. SymVal a => SList a -> SList a -> SList a
++ SList Integer
ys

        -- Program should never change values of @xs@ and @ys@
        noChange :: Stable A
noChange = [String -> (A -> SList Integer) -> A -> A -> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"xs" A -> SList Integer
forall a. AppS a -> a
xs, String -> (A -> SList Integer) -> A -> A -> (String, SBool)
forall a st.
EqSymbolic a =>
String -> (st -> a) -> st -> st -> (String, SBool)
stable String
"ys" A -> SList Integer
forall a. AppS a -> a
ys]

-- * Correctness

-- | We check that @zs@ is @xs ++ ys@ upon termination.
--
-- >>> correctness
-- Total correctness is established.
-- Q.E.D.
correctness :: IO (ProofResult (AppS [Integer]))
correctness :: IO (ProofResult (AppS [Integer]))
correctness = WPConfig -> Program A -> IO (ProofResult (AppS [Integer]))
forall st res.
(Show res, Mergeable st, Queriable IO st, res ~ QueryResult st) =>
WPConfig -> Program st -> IO (ProofResult res)
wpProveWith WPConfig
defaultWPCfg{wpVerbose=True} Program A
imperativeAppend