scyther-proof-0.3.0: Automatic generation of Isabelle/HOL correctness proofs for security protocols.

Text.Isar

Contents

Description

Generating Isabelle/ISAR theory files using Text.PrettyPrint.

Synopsis

ISAR Output

class Isar a whereSource

Values that can be output as ISAR code.

Minimal definition: isar

Methods

isar :: IsarConf -> a -> DocSource

Configuration

data IsarStyle Source

The ISAR style to be used for output.

Constructors

PlainText 
XSymbol 

data IsarConf Source

The configuration to be used for output. Apart from the ISAR style, the configuration also stores the representation of the reachable state of the protocol which we are reasoning about.

Constructors

IsarConf 

Fields

isarStyle :: IsarStyle
 
isarTrace :: Doc

The ISAR code of the trace

isarPool :: Doc

The ISAR code of the thread pool

isarSubst :: Doc

The ISAR code of the substitution

Instances

Show IsarConf 
MarkupMonad m => PrettyMonad (ReaderT IsarConf m)

Pretty printing as an ISAR theory file is accomplished by using a reader monad transformer with an ISAR output configuration as the environment.

defaultIsarConf :: IsarConfSource

Default configuration: plaintext ISAR style and reachable state (t,r,s).

isPlainStyle :: IsarConf -> BoolSource

Check if the plaintext style was chosen.

isarPlain :: Isar a => a -> DocSource

Output as ISAR code using defaultIsarConf.

isarXSymbol :: Isar a => a -> DocSource

Output as ISAR code using defaultIsarConf with the XSymbol style.

Constructions of our security protocol verification theory

isaExecutionSystemState :: IsarConf -> DocSource

Isabelle representation of the exeuction system state of our operational semantics.

Special Symbols

isarightArrow :: Document d => IsarConf -> dSource

A short right arrow: ->

isaLongRightArrow :: Document d => IsarConf -> dSource

A long double right arrow: ==>

isaLParr :: Document d => IsarConf -> dSource

A left parenthesis with an additional vertical line: (|

isaRParr :: Document d => IsarConf -> dSource

A right parenthesis with an additional vertical line: |)

isaLBrack :: Document d => IsarConf -> dSource

A left bracket with an additional vertical line: [|

isaRBrack :: Document d => IsarConf -> dSource

A right bracket with an additional vertical line: |]

isaMetaAll :: Document d => IsarConf -> dSource

The meta all quantifier: !!

isaExists :: Document d => IsarConf -> dSource

The exists symbol: ?

isaAnd :: Document d => IsarConf -> dSource

The logical and symbol: &

isaNotIn :: Document d => IsarConf -> dSource

A 'not in' symbol: ~:

isaIn :: Document d => IsarConf -> dSource

An 'in' symbol: :

isaSubsetEq :: Document d => IsarConf -> dSource

The non-strict subset symbol.

isaAlpha :: Document d => IsarConf -> dSource

The greek letter alpha: \alpha

isaSublocale :: Document d => IsarConf -> dSource

The sublocale sign.

Extensions of Text.PrettyPrint

nestBetweenSource

Arguments

:: Document d 
=> Int

Indent of body

-> d

Leading document

-> d

Finishing document

-> d

Body document

-> d 

Nest a document surrounded by a leading and a finishing document breaking lead, body, and finish onto separate lines, if they don't fit on a single line.

nestShortSource

Arguments

:: Document d 
=> Int

Indent of body

-> d

Leading document

-> d

Finishing document

-> d

Body document

-> d 

Nest a document surrounded by a leading and a finishing document with an non-compulsory break between lead and body.

nestShort' :: Document d => String -> String -> d -> dSource

Nest document between two strings and indent body by length lead + 1.

nestShortNonEmpty :: Document d => Int -> d -> d -> d -> dSource

Like nestShort but doesn't print the lead and finish, if the document is empty.

nestShortNonEmpty' :: Document d => String -> String -> d -> dSource

Like nestShort' but doesn't print the lead and finish, if the document is empty.

fixedWidthText :: Document d => Int -> String -> dSource

Output text with a fixed width: if it is smaller then nothing happens, otherwise care is taken to make the text appear having the given width.

symbol :: Document d => String -> dSource

Print string as symbol having width 1.

numbered :: Document d => d -> [d] -> dSource

Number a list of documents that are vertically separated by the given separator.

numbered' :: Document d => [d] -> dSource

Number a list of documents with numbers terminated by . and vertically separate using an empty line.