pics

examples/nonomitting/notebook.spec

@@ -5,15 +5,11 @@ loop {
 		forallmay x:User, i:Info
 			Written(i, x) → Read += (x, i)
 	} {
-		forall x:User, i:Info
-			Oracle(i, x) → Written += (i, x)
+		forallmay x:User, i:Info
+			True → Written += (i, x)
 	}
 }
 
-Declassify
-
-Oracle(i:Info,x:User): Written(i:Info, u:User)
-
 Target
 
 Read(u:User, info:Info)

examples/nonomitting/notebook_stubborn.spec

@@ -5,15 +5,11 @@ loop {
 		forallmay x:User, i:Info
 			Written(i, x) → Read += (x, i)
 	} {
-		forall x:User, i:Info
-			Oracle(i, x) → Written += (i, x)
+		forallmay x:User, i:Info
+			True → Written += (i, x)
 	}
 }
 
-Declassify
-
-Oracle(i:Info,x:User): Written(i:Info, u:User)
-
 Target
 
 Read(u:User, info:Info)