Commit f11bbc0a authored by Christian Müller's avatar Christian Müller

non-temporal declass

parent e3cd409a
......@@ -16,7 +16,7 @@ forallmay a,b
Declassify
O(x): F (T1(x))
O(x): T1(x)
Target
......
......@@ -18,7 +18,7 @@ forallmay a,b
Declassify
O(x): F (T1(x) ∨ T2(x))
O(x): (T1(x) ∨ T2(x))
Target
......
......@@ -13,7 +13,7 @@ loop {
Declassify
O(x:A,p:P): G ¬ Conf(at:A,p:P)
O(x:A,p:P): ¬ Conf(at:A,p:P)
Target
......
......@@ -13,7 +13,7 @@ loop {
Declassify
O(x:A,p:P,r:R): G ¬ Conf(at:A,p:P)
O(x:A,p:P,r:R): ¬ Conf(at:A,p:P)
Target
......
......@@ -11,7 +11,7 @@ forallmay y:X,x:X,p:P
Declassify
O(x:X,p:P,r:R): G ¬ Conf(xt:X,p:P)
O(x:X,p:P,r:R): ¬ Conf(xt:X,p:P)
Target
......
......@@ -12,7 +12,7 @@ loop {
Declassify
Oracle(i:Info,x:User): F (Written(i:Info, u:User))
Oracle(i:Info,x:User): Written(i:Info, u:User)
Target
......
......@@ -9,7 +9,7 @@ forallmay t:TA,s:Student
Declassify
O(p:Prof,s:Student,g:Grade): F Grading(p:Prof,as:Student,g:Grade)
O(p:Prof,s:Student,g:Grade): Grading(p:Prof,as:Student,g:Grade)
Target
......
......@@ -13,7 +13,7 @@ loop {
Declassify
O(x:A,p:P,r:R): G ¬ Conf(at:A,p:P)
O(x:A,p:P,r:R): ¬ Conf(at:A,p:P)
Target
......
......@@ -9,7 +9,7 @@ loop {
Declassify
O(x:A,p:P): G ¬ Conf(at:A,p:P)
O(x:A,p:P): ¬ Conf(at:A,p:P)
Target
......
......@@ -7,7 +7,7 @@ forall x:X,s:S
Declassify
O(x:X,s:S): G ¬ C(xt:X,s:S)
O(x:X,s:S): ¬ C(xt:X,s:S)
Target
......
......@@ -16,7 +16,7 @@ forallmay a,b
Declassify
O(x): F (T1(x) ∨ T2(x))
O(x): (T1(x) ∨ T2(x))
Target
......
......@@ -16,7 +16,7 @@ forallmay a,b
Declassify
O(x): F (T1(x) ∨ T2(x))
O(x): (T1(x) ∨ T2(x))
Target
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment