Update README.md

maciejpirog · Oct 1, 2020 · a34e0d3 · a34e0d3
1 parent f1e9ca0
commit a34e0d3
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/README.md b/README.md
@@ -102,6 +102,7 @@ LOG-EXPR ::= (B-OP LOG-EXPR ...)
           |  (forall (X ...) LOG-EXPR)
           |  (exists (X ...) LOG-EXPR)
           |  (REL A-EXPR ...)
+          |  (init X ...)
 ```
 
 where:
@@ -117,6 +118,8 @@ where:
 
 As a convention, we write verification logic expressions in curly braces (except of course the constants `true` and `false`) and we use all-caps for names of relations.
 
+`(init x y ... z)` stands for `(and (= x init-x) (= y init-y) ... (= z init-z))`.
+
 ### While
 
 ```