typedcausal3.spec 261 Bytes
Newer Older
Christian Müller's avatar
Christian Müller committed
1 2 3 4 5 6 7 8 9 10 11 12 13
Workflow

forall a:T1
    (O(a)) -> R += (a)
forallmay a:T1,b:T2
    True -> S += (b, a)
forallmay a:T2,b:T3
    True -> T += (b, a)
forallmay a:T3,b:T4
    True -> U += (b, a)

Declassify

14
O(x:T1): True
Christian Müller's avatar
Christian Müller committed
15 16 17

Target

Christian Müller's avatar
Christian Müller committed
18
U(a1:T4, a2:T3)
Christian Müller's avatar
Christian Müller committed
19 20 21 22

Causality

ca:T1, cb:T2, cc:T3