You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: website/docs/heyvl/statements.md
+97-38Lines changed: 97 additions & 38 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -8,14 +8,40 @@ sidebar_position: 2
8
8
Statements in HeyVL are instructions that are interpreted sequentially and that have side-effects.
9
9
They are used inside the body of [procedures](./procs.md).
10
10
11
-
## Semantics
11
+
We can categorize HeyVL's statements into either *concrete* or *verification* statements.
12
+
We have [concrete statements](#concrete-statements) and [verification statements](#verification-statements).
13
+
Concrete statements include [assignments](#assignments), [Boolean choices](#boolean-choices), and [while loops](#while-loops).
14
+
15
+
The purpose of *verification statements* is to encode either *proof obligations* and *proof assumptions*.
16
+
For example, [assert and assume statements](#assert-and-assume) are used to do this.
17
+
When you are verifying programs, you ideally do not use these verification statements directly but instead use Caesar's built-in set of [proof rules](../proof-rules/).
18
+
They internally use verification statements, but Caesar's proof rules guarantee correct usage so that the proofs are sound.
19
+
20
+
Below is an overview of HeyVL's statements with links to the respective documentation sections:
There are also some [deprecated verification statements](#deprecated-statements).
31
+
32
+
33
+
## Semantics: The Meaning of HeyVL Programs {#semantics}
12
34
13
35
Since HeyVL is an intermediate verification language, not all statements allow an operational interpretation of their effects.
14
36
All HeyVL statements should be understood through their (quantitative) verification condition semantics.
15
37
These are defined in reverse order, starting from an initial verification condition and proceeding from the last statement backwards to the front.
16
38
We describe the *formal semantics of HeyVL statements*[in our paper on Caesar (cf. Section 3)](https://arxiv.org/pdf/2309.07781.pdf#page=10).
17
39
18
-
## Blocks
40
+
41
+
## Concrete Statements
42
+
43
+
44
+
### Blocks
19
45
20
46
A block is a sequence of statements enclosed by curly braces.
21
47
Statements _may_ be separated by semicolons, but those can be omitted.
@@ -30,33 +56,82 @@ x = 1
30
56
y = 1 // y is not declared in this scope
31
57
```
32
58
33
-
## Variable Declarations
34
59
35
-
A variable declaration `var name: Type` creates a new local variable in the current scope.
60
+
### Variable Declarations
61
+
62
+
A variable declaration creates a new local variable of type `Type` in the current scope:
63
+
```heyvl
64
+
var name: Type
65
+
```
66
+
See the [standard library](../stdlib/) for Caesar's built-in types and [domains](./domains.md) for user-defined types.
67
+
36
68
A variable declaration can be combined with an assignment to initialize the variable:
37
69
```heyvl
38
70
var forty_two: UInt = 42
39
71
```
40
72
41
-
## Assignments
73
+
If a variable is not initialized, the program will be verified *for all* possible values of that variable.
42
74
43
-
An assignment `x = 39 + y` evaluates the expression on the right-hand side in the current state and assigns the result to the variable on the left-hand side.
75
+
### Assignments and Procedure Calls {#assignments}
76
+
77
+
An assignment evaluates the expression on the right-hand side in the current state and assigns the result to the variable on the left-hand side.
78
+
For example:
79
+
```heyvl
80
+
x = 39 + y
81
+
```
82
+
The right-hand side must evaluate to a value of a type that can be matches the type of `x`.
83
+
84
+
The right-hand side of the assignment can be a procedure call.
85
+
See the [reference on procedure calls](./procs.md#calling-procedures) for more information.[^calls-concrete]
44
86
45
87
The left-hand side of an assignment may be a list of variables to unpack a tuple.
46
88
For example, imagine a procedure `two_numbers` whose return type is `(x: UInt, y: UInt)`.
47
89
The following statement assigns the result of a call to `two_numbers` to `x` and `y`:
48
90
```heyvl
49
91
x, y = two_numbers()
50
92
```
93
+
If the procedure does not have any return values, the call may be written without the equals sign and the left-hand side, i.e. simply:
94
+
```heyvl
95
+
fn(arg1, arg2)
96
+
```
51
97
52
-
If the right-hand side of the assignment is a (pure) expression, then the verification condition semantics amounts to a substitution of the left-hand side by the right-hand side.
53
98
54
-
The right-hand side of the assignment can be a procedure call.
55
-
See the [reference on procedure calls](./procs.md#calling-procedures) for more information.
99
+
### Boolean Choices
100
+
101
+
HeyVL supports a binary choice depending on the value of a Boolean expression:
102
+
```heyvl
103
+
if x + 1 == 2 {
104
+
...
105
+
} else {
106
+
...
107
+
}
108
+
```
109
+
110
+
### While Loops
111
+
112
+
HeyVL supports while loops that run a block of code while a condition evaluates to true.
113
+
```heyvl
114
+
var cont: Bool = true
115
+
@invariant(...)
116
+
while cont {
117
+
cont = flip(0.5)
118
+
}
119
+
```
120
+
121
+
For verification, **while loops need to have [proof rule annotations](../proof-rules/)** such as the [`@invariant(...)` annotation](../proof-rules/induction.md) in the example.
122
+
If a while loop does not have a proof rule annotation, Caesar cannot verify the program and will show an error.
123
+
124
+
The proof rule annotations also implicitly specify whether the loop has least or greatest fixpoint semantics.
125
+
This choice can be made explicit with the [calculus annotations](../proof-rules/calculi.md) on procedures, which we recommend you use.
126
+
127
+
With the **[model checking translation](../model-checking.md), proof rule annotations are not necessary**.
128
+
It allows usage of a *probabilistic model checker* such as [Storm](https://www.stormchecker.org/) for a subset of HeyVL programs.
129
+
This can be helpful to e.g. get an initial estimation of expected values.
56
130
57
-
If the procedure does not have any return values, the call may be written without the equals sign and the left-hand side, i.e. simply `fn(arg1, arg2)`.
131
+
## Verification Statements
58
132
59
-
## Havoc
133
+
134
+
### Havoc
60
135
61
136
A `havoc` statement can be used to "forget" previous values of variables in the following code.
62
137
It also comes in a `co` variant.
@@ -67,7 +142,8 @@ cohavoc a, b, c
67
142
68
143
The verification condition semantics of `havoc` and `cohavoc` create an infimum respectively supremum over the specified variables.
69
144
70
-
## Assert and Assume
145
+
146
+
### Assert and Assume
71
147
72
148
These statements generate binary operators in the verification condition semantics.
73
149
All three statements also come in `co` variants.
@@ -79,7 +155,8 @@ assert 1 + x
79
155
assume 0
80
156
```
81
157
82
-
## Reward (formerly Tick)
158
+
159
+
### Reward
83
160
84
161
The `reward` statement accepts an expression and adds it to the current verification condition.
85
162
For example,
@@ -90,7 +167,8 @@ has the following semantics: `vc[reward 2 * x](f) = f + (2 * x)`.
90
167
91
168
`tick` is another name that Caesar accepts for `reward`.
92
169
93
-
## Nondeterministic Choices
170
+
171
+
### Nondeterministic Choices
94
172
95
173
HeyVL supports two kinds of binary nondeterministic choices: The "demonic" one (`if ⊓`) and the "angelic" one (`if ⊔`).
96
174
```heyvl
@@ -105,30 +183,6 @@ You can also use Latex-style syntax instead of Unicode.
105
183
Caesar supports `\cap` and `\cup` instead of `⊓` and `⊔`, respectively.
106
184
(We're looking for better syntax for these statements. If you have an idea, [please start a discussion](https://github.com/moves-rwth/caesar/discussions).)
107
185
108
-
## Boolean Choices
109
-
110
-
HeyVL supports a binary choice depending on the value of a Boolean expression:
111
-
```heyvl
112
-
if x + 1 == 2 {
113
-
...
114
-
} else {
115
-
...
116
-
}
117
-
```
118
-
119
-
## While Loops
120
-
121
-
HeyVL supports while loops that run a block of code while a condition evaluates to true.
122
-
```heyvl
123
-
var cont: Bool = true
124
-
while cont {
125
-
cont = flip(0.5)
126
-
}
127
-
```
128
-
129
-
However, for verification while loops need to be annotated with [proof rules](../proof-rules/), otherwise Caesar will show an error.
130
-
These proof rule annotations also implicitly specify whether the loop has least or greatest fixpoint semantics.
131
-
This choice can be made explicit with the [calculus annotations](../proof-rules/calculi.md) on procedures, which we recommend you use.
132
186
133
187
## Deprecated Statements
134
188
@@ -162,3 +216,8 @@ If negations are used in such a way that monotonicity is broken, then (co)proced
162
216
Refer to our [OOPSLA '23 paper](../publications.md#oopsla-23) for details on monotonicity and soundness of (co)procedure calls.
163
217
164
218
:::
219
+
220
+
221
+
[^calls-concrete]: Note that a procedure does not necessarily need to have a body.
222
+
Caesar will verify calls only based on their specification.
223
+
In those cases, a procedure call is thus not concrete.
0 commit comments