verifiable-expressions-0.6.0: An intermediate language for Hoare logic style verification.

Index

*&&Language.Expression.Prop, Language.Verification.Conditions
*->Language.Expression.Prop, Language.Verification.Conditions
*<->Language.Expression.Prop, Language.Verification.Conditions
*||Language.Expression.Prop, Language.Verification.Conditions
.&&Language.While.Syntax.Sugar
...Language.Expression.Util
.<Language.While.Syntax.Sugar
.<=Language.While.Syntax.Sugar
.=.Language.While.Syntax.Sugar
.==Language.While.Syntax.Sugar
.>Language.While.Syntax.Sugar
.>=Language.While.Syntax.Sugar
.||Language.While.Syntax.Sugar
abstractLanguage.Expression.Scope
abstractTraverseLanguage.Expression.Scope
AddLanguage.Expression.Example
allowQuantifiedQueriesLanguage.Verification
allSatMaxModelCountLanguage.Verification
allSatPrintAlongLanguage.Verification
AnnCommandLanguage.While.Hoare
AnnotationLanguage.Verification.Conditions
AnnSeqLanguage.Verification.Conditions
AsOp 
1 (Type/Class)Language.Expression.Choice
2 (Data Constructor)Language.Expression.Choice
Assignment 
1 (Type/Class)Language.Verification.Conditions
2 (Data Constructor)Language.Verification.Conditions
assignVCsLanguage.Verification.Conditions
BLanguage.Expression.Scope
boundVarLanguage.Expression.Scope
BVLanguage.Expression.Scope
CAnnLanguage.While.Syntax
CAssignLanguage.While.Syntax
castVarSymLanguage.Verification.Core, Language.Verification
chainSubLanguage.Verification.Conditions
checkPartialHoareLanguage.While.Hoare.Prover
choiceToUnionLanguage.Expression.Choice
ChooseOpLanguage.Expression.Choice
chooseOpLanguage.Expression.Choice
CIfLanguage.While.Syntax
cmdAnnSeqLanguage.Verification.Conditions
CmdAssignLanguage.Verification.Conditions
CommandLanguage.While.Syntax
CSeqLanguage.While.Syntax
CSkipLanguage.While.Syntax
CWhileLanguage.While.Syntax
defaultSMTCfgLanguage.Verification
emptyAnnSeqLanguage.Verification.Conditions
EqualLanguage.Expression.Example
eqVarTypesLanguage.Verification.Core, Language.Verification
evalManyLanguage.Expression.GeneralOp
EvalOpAtLanguage.Expression.GeneralOp
evalPropLanguage.Verification.Core, Language.Verification
evalProp'Language.Verification.Core, Language.Verification
evalPropSimpleLanguage.Verification.Core, Language.Verification
evalSimpleExprSymbolicLanguage.Expression.Example
evalVarSymbolicLanguage.Expression.Example
evalWhileExprLanguage.While.Syntax
evalXOrYLanguage.Expression.Example
exampleExprLanguage.Expression.Example
exampleExpr2Language.Expression.Example
examplePredicateLanguage.Expression.Example
exprLanguage.Expression.Prop, Language.Verification.Conditions
FLanguage.Expression.Scope
FailedLanguage.While.Syntax
foldBVLanguage.Expression.Scope
freeVarLanguage.Expression.Scope
GeneralOpLanguage.Expression.GeneralOp
generateVCsLanguage.While.Hoare
generateVCs'Language.While.Hoare
getHFree'Language.Expression.Choice
getQueryLanguage.Verification.Core
getVerifierLanguage.Verification.Core
hbifoldLanguage.Expression, Language.Verification
HBifoldableAtLanguage.Expression, Language.Verification
hbifoldMapLanguage.Expression, Language.Verification
hbifoldMapMonoidLanguage.Expression, Language.Verification
HBifunctorLanguage.Expression, Language.Verification
hbimapLanguage.Expression, Language.Verification
hbimapBVLanguage.Expression.Scope
HBindLanguage.Expression, Language.Verification
hbindTraverseLanguage.Expression, Language.Verification
HBitraversableLanguage.Expression, Language.Verification
hbitraverseLanguage.Expression, Language.Verification
hbitraverseBVLanguage.Expression.Scope
hbitraverseScopeLanguage.Expression.Scope
HBoundLanguage.Expression.Scope
HDuofoldableAtLanguage.Expression, Language.Verification
hduofoldMapLanguage.Expression, Language.Verification
HDuofunctorLanguage.Expression, Language.Verification
hduomapLanguage.Expression, Language.Verification
hduomapFirstLanguage.Expression, Language.Verification
hduomapFirst'Language.Expression, Language.Verification
hduomapSecondLanguage.Expression, Language.Verification
HDuotraversableLanguage.Expression, Language.Verification
hduotraverseLanguage.Expression, Language.Verification
hduotraverseFirstLanguage.Expression, Language.Verification
hduotraverseFirst'Language.Expression, Language.Verification
hduotraverseSecondLanguage.Expression, Language.Verification
hfirstLanguage.Expression, Language.Verification
hfoldLanguage.Expression, Language.Verification
hfoldALanguage.Expression, Language.Verification
HFoldableAtLanguage.Expression, Language.Verification
hfoldMapLanguage.Expression, Language.Verification
hfoldMapALanguage.Expression, Language.Verification
hfoldMapMonoidLanguage.Expression, Language.Verification
hfoldTraverseLanguage.Expression, Language.Verification
HFreeLanguage.Expression, Language.Verification
HFree' 
1 (Type/Class)Language.Expression.Choice
2 (Data Constructor)Language.Expression.Choice
HFunctorLanguage.Expression, Language.Verification
hjoinLanguage.Expression, Language.Verification
hliftMLanguage.Expression, Language.Verification
hmapLanguage.Expression, Language.Verification
HMonadLanguage.Expression, Language.Verification
HPointedLanguage.Expression, Language.Verification
HPureLanguage.Expression, Language.Verification
hpureLanguage.Expression, Language.Verification
hsecondLanguage.Expression, Language.Verification
hsequenceLanguage.Expression, Language.Verification
HTraversableLanguage.Expression, Language.Verification
htraverseLanguage.Expression, Language.Verification
HWrapLanguage.Expression, Language.Verification
hwrap'Language.Expression.Choice
IfThenElseLanguage.Expression.Example
ifThenElseLanguage.Expression.Example
ifVCsLanguage.Verification.Conditions
ignoreExitCodeLanguage.Verification
implHduofoldMapLanguage.Expression, Language.Verification
implHduofoldMapComposeLanguage.Expression, Language.Verification
implHfoldMapLanguage.Expression, Language.Verification
implHfoldMapComposeLanguage.Expression, Language.Verification
isNonModelVarLanguage.Verification
JoinAnnSeq 
1 (Type/Class)Language.Verification.Conditions
2 (Data Constructor)Language.Verification.Conditions
joinAnnSeqLanguage.Verification.Conditions
joiningAnnSeqLanguage.Verification.Conditions
JustAssignLanguage.Verification.Conditions
liftScopeLanguage.Expression.Scope
liftSymbolicLanguage.Verification.Core
litLanguage.Expression.Example
LiteralLanguage.Expression.Example
LogAndLanguage.Expression.Prop, Language.Verification.Conditions
LogEquivLanguage.Expression.Prop, Language.Verification.Conditions
LogicOpLanguage.Expression.Prop, Language.Verification.Conditions
LogImplLanguage.Expression.Prop, Language.Verification.Conditions
LogLitLanguage.Expression.Prop, Language.Verification.Conditions
LogNotLanguage.Expression.Prop, Language.Verification.Conditions
LogOrLanguage.Expression.Prop, Language.Verification.Conditions
lookupVarLanguage.While.Syntax
MonadGenLanguage.While.Hoare
multiIfVCsLanguage.Verification.Conditions
noOpsLanguage.Expression.Choice
oneStepLanguage.While.Syntax
OpLanguage.Expression.GeneralOp
OpAddLanguage.While.Syntax
OpAndLanguage.While.Syntax
OpChoiceLanguage.Expression.Choice
OpEqLanguage.While.Syntax
OpGELanguage.While.Syntax
OpGTLanguage.While.Syntax
OpLELanguage.While.Syntax
OpLitLanguage.While.Syntax
OpLTLanguage.While.Syntax
OpMulLanguage.While.Syntax
OpNotLanguage.While.Syntax
OpOrLanguage.While.Syntax
OpSubLanguage.While.Syntax
OpThatLanguage.Expression.Choice
OpThisLanguage.Expression.Choice
optimizeValidateConstraintsLanguage.Verification
plitLanguage.Expression.Prop, Language.Verification.Conditions
pnotLanguage.Expression.Prop, Language.Verification.Conditions
PrettyLanguage.Expression.Pretty
prettyLanguage.Expression.Pretty
Pretty1Language.Expression.Pretty
pretty1Language.Expression.Pretty
Pretty2Language.Expression.Pretty
pretty2Language.Expression.Pretty
Pretty3Language.Expression.Pretty
pretty3Language.Expression.Pretty
PrettyOpLanguage.Expression.GeneralOp
prettysLanguage.Expression.Pretty
prettys1Language.Expression.Pretty
prettys1BinopLanguage.While.Syntax
prettys1PrecLanguage.Expression.Pretty
prettys1PrecBinopLanguage.Expression.Pretty
prettys1PrecUnopLanguage.Expression.Pretty
prettys2Language.Expression.Pretty
prettys2PrecLanguage.Expression.Pretty
prettys3Language.Expression.Pretty
prettys3PrecLanguage.Expression.Pretty
prettysPrecLanguage.Expression.Pretty
prettysPrecOpLanguage.Expression.GeneralOp
printBaseLanguage.Verification
printRealPrecLanguage.Verification
ProgressLanguage.While.Syntax
PropLanguage.Expression.Prop, Language.Verification.Conditions
Prop'Language.Expression.Prop, Language.Verification.Conditions
propAndLanguage.Expression.Prop, Language.Verification.Conditions
PropAnn 
1 (Type/Class)Language.While.Hoare
2 (Data Constructor)Language.While.Hoare
propAnnSeqLanguage.Verification.Conditions
propOrLanguage.Expression.Prop, Language.Verification.Conditions
provePartialHoareLanguage.While.Hoare.Prover
putPrettyLanguage.Expression.Pretty
Query 
1 (Type/Class)Language.Verification.Core, Language.Verification
2 (Data Constructor)Language.Verification.Core
queryLanguage.Verification.Core, Language.Verification
QueryStateLanguage.Verification.Core
redirectVerboseLanguage.Verification
roundingModeLanguage.Verification
runCommandLanguage.While.Syntax
runVerifierLanguage.Verification.Core, Language.Verification
runVerifierWithLanguage.Verification.Core, Language.Verification
satCmdLanguage.Verification
satTrackUFsLanguage.Verification
Scope 
1 (Type/Class)Language.Expression.Scope
2 (Data Constructor)Language.Expression.Scope
Scoped 
1 (Type/Class)Language.Expression.Scope
2 (Data Constructor)Language.Expression.Scope
sequenceVCsLanguage.Verification.Conditions
SFreeLanguage.Expression.Scope
SimpleExprLanguage.Expression.Example
SimpleOpLanguage.Expression.Example
SimpleVar 
1 (Type/Class)Language.Expression.Example
2 (Data Constructor)Language.Expression.Example
skipVCsLanguage.Verification.Conditions
SMTConfig 
1 (Data Constructor)Language.Verification
2 (Type/Class)Language.Verification
smtLibVersionLanguage.Verification
solverLanguage.Verification
solverSetOptionsLanguage.Verification
SomeSym 
1 (Type/Class)Language.Verification.Core
2 (Data Constructor)Language.Verification.Core
splitSeqLanguage.While.Hoare
SPureLanguage.Expression.Scope
squashExpressionLanguage.Expression.Choice
StepResultLanguage.While.Syntax
subAssignmentLanguage.Verification.Conditions
SubsetOpLanguage.Expression.Choice
subsetOpLanguage.Expression.Choice
subVarLanguage.Verification.Core, Language.Verification
SWrapLanguage.Expression.Scope
symbolVarLanguage.Verification.Core
symForVarLanguage.Verification.Core, Language.Verification
TerminatedLanguage.While.Syntax
testLanguage.While.Test
testCommandAnnLanguage.While.Test
testConfigLanguage.While.Test
testPostcondLanguage.While.Test
testPrecondLanguage.While.Test
testVcsLanguage.While.Test
throwQueryLanguage.Verification.Core
timingLanguage.Verification
transcriptLanguage.Verification
TripletLanguage.Verification.Conditions
tryJoinAnnSeqLanguage.Verification.Conditions
unionToChoiceLanguage.Expression.Choice
unscopeLanguage.Expression.Scope
unscopedLanguage.Expression.Scope
validateModelLanguage.Verification
varLanguage.Expression.Example
VarEnvLanguage.Verification.Core, Language.Verification
VarKeyLanguage.Verification.Core, Language.Verification
varKeyLanguage.Verification.Core, Language.Verification
VarSymLanguage.Verification.Core, Language.Verification
VEMismatchedSymbolTypeLanguage.Verification.Core, Language.Verification
verboseLanguage.Verification
VerifiableVarLanguage.Verification.Core, Language.Verification
Verifier 
1 (Type/Class)Language.Verification.Core, Language.Verification
2 (Data Constructor)Language.Verification.Core
VerifierErrorLanguage.Verification.Core, Language.Verification
VESbvExceptionLanguage.Verification.Core, Language.Verification
wenotLanguage.While.Syntax.Sugar
WhileExprLanguage.While.Syntax
WhileOpLanguage.While.Syntax
WhileOpKindLanguage.While.Syntax
WhilePropLanguage.While.Hoare
WhileVar 
1 (Type/Class)Language.While.Syntax
2 (Data Constructor)Language.While.Syntax
whileVCsLanguage.Verification.Conditions
\\Language.While.Syntax.Sugar
^+Language.Expression.Example
^==Language.Expression.Example
^>>=Language.Expression, Language.Verification
^>>>=Language.Expression.Scope
^^^Language.While.Syntax.Sugar
_OpChoiceLanguage.Expression.Choice
_OpThatLanguage.Expression.Choice
_OpThisLanguage.Expression.Choice
_ScopeLanguage.Expression.Scope
_ScopedLanguage.Expression.Scope