declasstest.spec 268 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
14
15
16
Workflow

forallmay x:A,p:P
	True -> Conf += (x,p)
loop {
	forall xa:A,xb:A,p:P (!Conf(xa,p) ∧ Acc(xb,p)) -> Read += (xa,xb,p)
	forallmay x:A,p:P (!Conf(x,p) ∧ O(x,p)) → Acc += (x,p)
}

Declassify

O(x:A,p:P): G ¬ Conf(at:A,p:P)

Target

Read(at:A, bt:A, pt:P)