Relational interpretation of PDL programs

DefinitionRelational interpretation of a PDL program#✓fully proved

Interpret a PDL program in CSLib's canonical relation algebra.

def Program.toRelation (M : Model World Atom Label)
    (a : Program Atom Label) : SquareRelations World :=
  {(s, t) | ProgRel M a s t}

Uses 3 · Used by 11

Statement usesPDL model · Relation denoted by a PDL program · PDL programs

Used byPartial correctness as inclusion in the relational core · Hoare triples as KAT absorption equations · Hoare triples as KAT test inequalities · Test absorption lifts through iteration · Loop exit absorption from a guarded-body absorption equation · Semantic completeness of the while-loop invariant rule · Relational interpretation preserves executions · Choice is interpreted by relational union · Sequencing is interpreted by relational composition · Iteration is interpreted by reflexive-transitive closure · Tests are interpreted by PDL satisfaction

TheoremRelational interpretation preserves executions#✓fully proved

The representation conversion preserves exactly the executions.

@[simp] theorem Program.mem_toRelation (M : Model World Atom Label)
    (a : Program Atom Label) (s t : World) :
    a.toRelation M (s, t) ↔ ProgRel M a s t

Uses 4

Statement usesPDL model · Relation denoted by a PDL program · PDL programs · Relational interpretation of a PDL program

TheoremSequencing is interpreted by relational composition#✓fully proved

The interpretation of sequencing uses canonical composition.

@[simp] theorem Program.toRelation_seq (M : Model World Atom Label)
    (a b : Program Atom Label) :
    (a.seq b).toRelation M = a.toRelation M * b.toRelation M

Uses 3

Statement usesPDL model · PDL programs · Relational interpretation of a PDL program

TheoremChoice is interpreted by relational union#✓fully proved

The interpretation of choice uses canonical union.

@[simp] theorem Program.toRelation_choice (M : Model World Atom Label)
    (a b : Program Atom Label) :
    (a.choice b).toRelation M = a.toRelation M ⊔ b.toRelation M

Uses 3

Statement usesPDL model · PDL programs · Relational interpretation of a PDL program

TheoremTests are interpreted by PDL satisfaction#✓fully proved

Formula tests use the existing PDL satisfaction predicate.

@[simp] theorem Program.toRelation_test (M : Model World Atom Label)
    (φ : Formula Atom Label) :
    (Program.test φ).toRelation M = testSet {s | Sat M φ s}

Uses 6

Statement usesPDL formulas · PDL model · PDL programs · Relational interpretation of a PDL program · Satisfaction of PDL formulas · Diagonal test relation of an assertion

TheoremIteration is interpreted by reflexive-transitive closure#✓fully proved

Iteration in the canonical carrier is the same reflexive-transitive closure as in ProgRel, including its identity boundary.

@[simp] theorem Program.toRelation_star (M : Model World Atom Label)
    (a : Program Atom Label) :
    a.star.toRelation M = {(s, t) |
      Relation.ReflTransGen (fun x y => a.toRelation M (x, y)) s t}

Uses 3

Statement usesPDL model · PDL programs · Relational interpretation of a PDL program

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.