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