Contents Index

SpecLanguage.Theory

Contents Syntax Rule helpers Rules

Description

This implements "A pure, sound, and complete (in the sense of Cook) Hoare logic for a language with specification statements and recursion", February 27, 1997, by Kai Engelhardt and Willem-Paul de Roever.

Synopsis

module Core.Utils module SpecLanguage.PFormula newtype SProg = SProg { code :: SCode } type SCode = Code SSyn data SSyn = Spec PFormula PFormula | Seq | Choice | RecDef String | RecCall String mkRuleResult_ :: SProg -> Region -> (SCode, [Condition]) -> Either Error (RuleResult SProg) substitution :: String -> SCode -> SCode -> SCode compFun :: SCode -> PFormula -> Maybe SCode choiceFun :: SCode -> Maybe SCode consFun :: SCode -> PFormula -> PFormula -> Maybe (SCode, [Condition]) recFun :: SCode -> String -> SProg -> Maybe (SCode, [Condition]) rules :: [Rule SProg]

Documentation

module Core.Utils

module SpecLanguage.PFormula

Syntax

newtype SProg

We have to wrap the code in a constructor, so that we can derive Typeable. Constructors SProg code :: SCode Instances Show SProg RuleResultSrc SCode SProg RuleResultSrc (SCode, [Condition]) SProg

type SCode = Code SSyn

data SSyn

Constructors Spec PFormula PFormula Seq Choice RecDef String RecCall String Instances Eq SSyn Read SSyn Show SSyn Syn SSyn

Rule helpers

mkRuleResult_ :: SProg -> Region -> (SCode, [Condition]) -> Either Error (RuleResult SProg)

substitution :: String -> SCode -> SCode -> SCode

Rules

compFun :: SCode -> PFormula -> Maybe SCode

choiceFun :: SCode -> Maybe SCode

consFun :: SCode -> PFormula -> PFormula -> Maybe (SCode, [Condition])

recFun :: SCode -> String -> SProg -> Maybe (SCode, [Condition])

The rule for recursion is modelled after the programmers' intuition that, if a recursive procedure works based on the assumption that all recursive calls work, then the recusive procedure works. (To work here means to behave according to specifications.)

rules :: [Rule SProg]

Produced by Haddock version 0.8