Documentation

EqCheckingAbstractInterpretation.Trace.RunningExample

Running Example: Abstract Trace Differences #

This file formalizes the running example for abstract trace differences. We instantiate the abstract difference computation AbstractDiff for the example with processes:

PA = a.PA + a.b.0 (the P_A of the note) PB = a.(PB + b.0) (the P_B of the note) PBb0 = PB + b.0 (the reachable intermediate state) b0 = b.0 (the stopping process)

Key results:

  1. abstractDiff_PBb0_b0 : marker present for (PBb0, {b0}) → not-preordered
  2. not_abstractDiff_b0_PBb0 : marker absent for (b0, {PBb0}) → b0 ≤ PBb0
  3. not_abstractDiff_PA_PB : marker absent for (PA, {PB}) → PA ≡ PB
source
theorem EqCheckingAbstractInterpretation.Trace.RunningExample.b0_no_a_deriv (p : CCS.RunningExample.RunProc) :
¬CCS.Deriv CCS.RunningExample.runEnv CCS.RunningExample.b0 CCS.RunningExample.RunAct.a p

b.0 has no a-derivative.

source
theorem EqCheckingAbstractInterpretation.Trace.RunningExample.derivSetOf_b0_a_empty :
CCS.DerivSetOf CCS.RunningExample.runEnv {CCS.RunningExample.b0} CCS.RunningExample.RunAct.a = fun (x : CCS.CCS CCS.RunningExample.RunAct CCS.RunningExample.RunName) => False

The a-shifted set of {b.0} is empty: b.0 has no a-derivative.

source
theorem EqCheckingAbstractInterpretation.Trace.RunningExample.abstractDiff_PBb0_b0 :
AbstractDiff CCS.RunningExample.runEnv CCS.RunningExample.PBb0 {CCS.RunningExample.b0}

Abstract trace difference is present for (PBb0, {b0}).

Derivation (two-step lfp construction):

  • step: PBb0 --a--> PBb0, shifted set Der({b.0}, a) = ∅
  • base: the empty competitor set triggers the base case of DTrSharp.
source
theorem EqCheckingAbstractInterpretation.Trace.RunningExample.b0_le_PBb0 :
TracePreorder CCS.RunningExample.runEnv CCS.RunningExample.b0 CCS.RunningExample.PBb0

Every trace of b0 is also a trace of PBb0: b0 = b.0 can only do b to 0, and PBb0 = PB + b.0 can also do b to 0.

source
theorem EqCheckingAbstractInterpretation.Trace.RunningExample.PA_le_PB :
TracePreorder CCS.RunningExample.runEnv CCS.RunningExample.PA CCS.RunningExample.PB

Every trace of PA is also a trace of PB.

Proved by simultaneous induction on TraceSem: for every reachable successor state p of PA (i.e. p ∈ {PA, b0, zero}), every trace of p is also a trace of the corresponding PB-side state.

source
def EqCheckingAbstractInterpretation.Trace.RunningExample.runAbstractDiff (state : CCS.RunningExample.RunProc) (competitors : FiniteLTS.StateSet CCS.RunningExample.RunProc) :
Bool

Executable marker query for the running example.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem EqCheckingAbstractInterpretation.Trace.RunningExample.runAbstractDiff_PA_PB :
    runAbstractDiff CCS.RunningExample.PA {CCS.RunningExample.PB} = false

    #eval runAbstractDiff PA {PB} #eval FiniteLTS.tracePreordered runLTS PA PB #eval runAbstractDiff PBb0 {b0}

    source
    theorem EqCheckingAbstractInterpretation.Trace.RunningExample.runAbstractDiff_PBb0_b0 :
    runAbstractDiff CCS.RunningExample.PBb0 {CCS.RunningExample.b0} = true
    source
    theorem EqCheckingAbstractInterpretation.Trace.RunningExample.runAbstractDiff_b0_PBb0 :
    runAbstractDiff CCS.RunningExample.b0 {CCS.RunningExample.PBb0} = false
    source
    theorem EqCheckingAbstractInterpretation.Trace.RunningExample.runAbstractDiff_b0_PBb0_correct :
    runAbstractDiff CCS.RunningExample.b0 {CCS.RunningExample.PBb0} = true ↔ AbstractDiff CCS.RunningExample.runEnv CCS.RunningExample.b0 {CCS.RunningExample.PBb0}

    The executable result for (b0, {PBb0}) agrees with AbstractDiff.

    source
    theorem EqCheckingAbstractInterpretation.Trace.RunningExample.runAbstractDiff_PA_PB_correct :
    runAbstractDiff CCS.RunningExample.PA {CCS.RunningExample.PB} = true ↔ AbstractDiff CCS.RunningExample.runEnv CCS.RunningExample.PA {CCS.RunningExample.PB}

    The executable result for (PA, {PB}) agrees with AbstractDiff.

    source
    theorem EqCheckingAbstractInterpretation.Trace.RunningExample.not_abstractDiff_b0_PBb0 :
    ¬AbstractDiff CCS.RunningExample.runEnv CCS.RunningExample.b0 {CCS.RunningExample.PBb0}

    Abstract trace difference is absent for (b0, {PBb0}).

    source
    theorem EqCheckingAbstractInterpretation.Trace.RunningExample.not_abstractDiff_PA_PB :
    ¬AbstractDiff CCS.RunningExample.runEnv CCS.RunningExample.PA {CCS.RunningExample.PB}

    Abstract trace difference is absent for (PA, {PB}).