Merge

Author: marcoeilers

src/SUMMARY.md

@@ -3,51 +3,51 @@
 - [Introduction](./introduction.md)
 - [Structure](./structure.md)
 - [Language Overview](./language.md)
-  - [Top-level declarations](./language-top.md)
-  - [Built-in types](./language-types.md)
-  - [Imports](./language-imports.md)
-  - [Annotations](./language-annotations.md)
+    - [Top-level declarations](./language-top.md)
+    - [Built-in types](./language-types.md)
+    - [Imports](./language-imports.md)
+    - [Annotations](./language-annotations.md)
 - [Permissions](./permissions.md)
-  - [Viper's program state](./permissions-state.md)
-  - [Inhaling and exhaling](./permissions-inhale-exhale.md)
-  - [Self-framing assertions](./permissions-self-framing.md)
-  - [Exclusive permissions](./permissions-exclusive.md)
-  - [Fractional permissions](./permissions-fractional.md)
+    - [Viper's program state](./permissions-state.md)
+    - [Inhaling and exhaling](./permissions-inhale-exhale.md)
+    - [Self-framing assertions](./permissions-self-framing.md)
+    - [Exclusive permissions](./permissions-exclusive.md)
+    - [Fractional permissions](./permissions-fractional.md)
 - [Predicates](./predicates.md)
 - [Functions](./functions.md)
 - [Quantifiers](./quantifiers.md)
 - [Quantified Permissions](./quantified-permissions.md)
-  - [Receiver expressions and injectivity](./quantified-permissions-injectivity.md)
+    - [Receiver expressions and injectivity](./quantified-permissions-injectivity.md)
 - [Magic Wands](./magic-wands.md)
-  - [Package operations](./magic-wands-package.md)
-  - [Heap-dependent expressions](./magic-wands-heap-dependent.md)
+    - [Package operations](./magic-wands-package.md)
+    - [Heap-dependent expressions](./magic-wands-heap-dependent.md)
 - [Statements](./statements.md)
-  - [Assignments](./statements-assignments.md)
-  - [Control structures](./statements-control.md)
-  - [Assertion checking](./statements-assertions.md)
-  - [Verifier directives](./statements-verifier.md)
+    - [Assignments](./statements-assignments.md)
+    - [Control structures](./statements-control.md)
+    - [Assertion checking](./statements-assertions.md)
+    - [Verifier directives](./statements-verifier.md)
 - [Expressions](./expressions.md)
-  - [Integer expressions](./expressions-integer.md)
-  - [Boolean expressions](./expressions-boolean.md)
-  - [Reference expressions](./expressions-reference.md)
-  - [Perm expressions](./expressions-perm.md)
-  - [Sequence expressions](./expressions-sequence.md)
-  - [Set and multiset expressions](./expressions-set-multiset.md)
-  - [Map expressions](./expressions-map.md)
-  - [Expressions of multiple types](./expressions-multi.md)
+    - [Integer expressions](./expressions-integer.md)
+    - [Boolean expressions](./expressions-boolean.md)
+    - [Reference expressions](./expressions-reference.md)
+    - [Perm expressions](./expressions-perm.md)
+    - [Sequence expressions](./expressions-sequence.md)
+    - [Set and multiset expressions](./expressions-set-multiset.md)
+    - [Map expressions](./expressions-map.md)
+    - [Expressions of multiple types](./expressions-multi.md)
 - [Assertions](./assertions.md)
 - [Domains](./domains.md)
-  - [Declaring new types](./domains-new-types.md)
-  - [Axiomatising custom theories](./domains-axiomatising.md)
-  - [Encoding an array datatype](./domains-array.md)
-  - [ADT plugin](./domains-adt.md)
+    - [Declaring new types](./domains-new-types.md)
+    - [Axiomatising custom theories](./domains-axiomatising.md)
+    - [Encoding an array datatype](./domains-array.md)
+    - [ADT plugin](./domains-adt.md)
 - [Termination](./termination.md)
-  - [Termination measures and `decreases` clauses](./termination-measures.md)
-  - [General syntax of `decreases` tuples](./termination-syntax.md)
-  - [Special `decreases` tuples](./termination-special-tuples.md)
-  - [Custom well-founded orders](./termination-custom-orders.md)
-  - [Mutual recursion](./termination-mutual-recursion.md)
-  - [Conditional termination](./termination-conditional.md)
-  - [Abstract functions](./termination-abstract.md)
-  - [Statement termination (experimental)](./termination-statement.md)
+    - [Termination measures and `decreases` clauses](./termination-measures.md)
+    - [General syntax of `decreases` tuples](./termination-syntax.md)
+    - [Special `decreases` tuples](./termination-special-tuples.md)
+    - [Custom well-founded orders](./termination-custom-orders.md)
+    - [Mutual recursion](./termination-mutual-recursion.md)
+    - [Conditional termination](./termination-conditional.md)
+    - [Abstract functions](./termination-abstract.md)
+    - [Statement termination (experimental)](./termination-statement.md)
 - [Further Information](./further-info.md)

src/domains.md

@@ -15,7 +15,7 @@ domain MyDomain {
 
 The functions declared in a domain are global: one can apply them in any other scope of the Viper program. Functions declared inside a domain are called *domain functions*; these are more restricted than the standard Viper functions described previously. In particular, domain functions cannot have preconditions; they can be applied in *any* state. They are also always abstract, i.e., cannot have a defined body. The typical way to attach any meaning to these otherwise-uninterpreted functions, is via domain axioms.
 
-Domain axioms are also global: they define properties of the program which are assumed to hold *in all states*. Since there is no restriction on the states to which an axiom applies, it must be well-defined in all states; for this reason, domain axioms cannot refer to the values of heap locations, nor to permission amounts (e.g., via [perm expressions](./expressions-perm.md)). In practice, domain axioms are standard (often quantified) first-order logic assertions. Axiom names are used only for readability of the code, but are currently not optional.
+Domain axioms are also global: they define properties of the program which are assumed to hold *in all states*. Since there is no restriction on the states to which an axiom applies, it must be well-defined in all states; for this reason, domain axioms cannot refer to the values of heap locations, nor to permission amounts (e.g., via [perm expressions](./expressions-perm.md)). In practice, domain axioms are standard (often quantified) first-order logic assertions. Axiom names are optional and are used only for readability of the code; for example, `axiom { bar(true) }` declares a valid, anonymous axiom.
 
 ```viper,editable,playground
 domain Neg {

src/expressions-perm.md

@@ -2,12 +2,12 @@
 
 Expressions of type `Perm` are real numbers and are usually used to represent permission amounts (though they can be used for other purposes).
 
-* Fractional permission expressions `e1/e2`, where both `e1` and `e2` are integers, evaluate to a Perm value whose numerator is `e1` and whose denominator is `e2`. A well-definedness condition is that `e2` must not equal 0. `e1/e2` can also denote a permission amount divided by an integer if `e1` is an expression of type `Perm` and `e2` is an expression of type `Int`.
+* Fractional permission expressions `e1/e2`, where both `e1` and `e2` are integers, evaluate to a Perm value whose numerator is `e1` and whose denominator is `e2`. A well-definedness condition is that `e2` must not equal 0. `e1/e2` can also denote a permission amount divided by an integer if `e1` is an expression of type `Perm` and `e2` is an expression of type `Int`, or the quotient of two permission amounts if both `e1` and `e2` are of type `Perm`. Note that for ambiguous cases like `1/2`, the division operator `/` defaults to `Perm`-typed division; `Int`-typed (truncating) division can be forced with the alternative syntax `e1 \ e2` (see the [section on integer expressions](./expressions-integer.md)).
 
 * The `Perm`-typed literals `none` and  `write` denote no permission and a full permission, corresponding to `0/1` and `1/1`, respectively.
 
 * The special literal `wildcard` denotes an unspecified positive amount. The specific value represented by `wildcard` is not fixed but is chosen anew every time a `wildcard` expression is encountered. In particular, if a `wildcard` amount of permission to a field or predicate is to be exhaled, a value less than the currently held amount is chosen, so that it is always possible to exhale (or assert having) a `wildcard` amount of any permission, unless no permission at all is currently held. However, exhaling and subsequently inhaling a `wildcard` permission to a location will not restore the initial permission amount, since it will not be known that the inhaled `wildcard` amount is equal to the exhaled one. The `wildcard` permission amount provides a convenient way to implement duplicable read-only resources, which, for example, can be used to model immutable data.
 
 * `perm(e.f)`: Evaluates to the amount of permission the current method has to the specified location. Similarly, `perm(P(e1, ..., en))` returns the amount of permission held for the specified predicate instance. Similarly to `forperm`, the values of `perm` expressions take into account the side-effects of e.g. ongoing `exhale` operations. For example `exhale acc(x.f) && perm(x.f) > none` should always fail, while `exhale perm(x.f) > none && acc(x.f)` will succeed (if the full permission to `x.f` was held before the `exhale`).
 
-* Permissions can be added (`e1 + e2`), subtracted (`e1 - e2`), multiplied (`e1 * e2`) or divided (`e1 / e2`). In the first two cases, `e1` and `e2` must both be `Perm`-typed. In the case of multiplication, either two `Perm`-typed expressions or one `Perm`-typed and one `Int`-typed are possible. For divisions, the first expression must be `Perm`-typed and the second of type `Int` (though of course ordinary fractions, where both expressions are `Int`-typed, also exist). The results in all cases will be `Perm`-typed expressions.
+* Permissions can be added (`e1 + e2`), subtracted (`e1 - e2`), multiplied (`e1 * e2`) or divided (`e1 / e2`). In the first two cases, `e1` and `e2` must both be `Perm`-typed. In the case of multiplication, either two `Perm`-typed expressions or one `Perm`-typed and one `Int`-typed are possible. For divisions, either both expressions are `Perm`-typed, or the first is `Perm`-typed and the second of type `Int` (and of course ordinary fractions, where both expressions are `Int`-typed, also exist). The results in all cases will be `Perm`-typed expressions.

src/functions.md

@@ -50,6 +50,8 @@ function capacity(l:Ref): Int
 
 Note that functions declared in [Viper domains (i.e. *domain functions*)](./domains.md) are considered by Viper to be abstract state-independent total functions. As such, they can neither have a body nor be equipped with any pre-/postconditions; see the [domains section](./domains.md) for more details. In contrast, top-level functions can be state-dependent; the ability for function preconditions to include permissions allows them to depend on not only the values of their parameters, but also on heap locations to which their preconditions require permissions.
 
+Permission *amounts* in function preconditions are interpreted differently from those in method preconditions: since functions cannot modify the heap, all that matters is whether a function may *read* a location, i.e., whether it has a positive permission amount. Concrete permission amounts in function preconditions are therefore ignored (and Viper reports a warning if one is written): `acc(x.f, 1/2)`, `acc(x.f, wildcard)` and `acc(x.f)` all simply require *some* positive permission to `x.f`. Two consequences are worth pointing out. First, non-aliasing cannot be concluded from permission amounts in a function precondition; e.g., unlike in a method precondition, `acc(x.f) && acc(y.f)` does *not* imply `x != y` inside the function. Second, inside a function, a predicate instance may be unfolded (via an [`unfolding` expression](./expressions-multi.md)) even if the precondition only provides a fraction of it. The previous behaviour, in which concrete permission amounts in function preconditions were taken into account, can be restored with the command-line option `--respectFunctionPrePermAmounts`.
+
 Viper checks that the function body and any postconditions are framed by the preconditions; that is, the preconditions must require all permissions that are needed to evaluate the function body and the postconditions. Moreover, Viper verifies that the postconditions can be proven to hold for the result of the function.
 In order to enable function termination checks, which are *not* performed by default, users can specify termination measures, as discussed in [the chapter on termination](./termination.md).
 As the checking of a recursive function definition is essentially a proof by induction on the unrolling of the definition, not checking termination can lead to unsound behaviour. The following example yields such an inconsistency by means of a non-terminating function:

src/introduction.md

@@ -4,7 +4,7 @@
 
 <img src="https://www.ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/images/Research/viper_architecture.png" alt="The Viper verification infrastructure" style="width: 100%;"/>
 
-The Viper infrastructure, shown above, provides an intermediate language as well as two verification back-ends, one based on symbolic execution and one based on verification condition generation. Both back-ends ultimately use the SMT solver
+The Viper infrastructure, shown above, provides an intermediate language as well as two verification back-ends: Viper's Symbolic Execution (SE) backend and its Verification Condition Generation (VCG) backend. Both back-ends ultimately use the SMT solver
 [Z3](https://github.com/Z3Prover/z3) to discharge proof obligations. Front-end tools translate different source languages and verification
 approaches into the Viper language and thereby benefit from its tool support and automation.
 

src/language-types.md

@@ -3,7 +3,7 @@
 * `Ref` for references (to objects, except for the built-in `Ref` constant `null`)
 * `Bool` for Boolean values
 * `Int` for mathematical (unbounded) integers
-* `Rational` for mathematical (unbounded) rationals (this type is expected to be deprecated in the summer 2023 release)
+* `Rational` for mathematical (unbounded) rationals (this type is deprecated and will be removed in a future release; use `Perm` instead)
 * `Perm` for permission amounts (see the [section on permissions](./permissions.md) for details)
 * `Seq[T]` for immutable sequences with element type `T`
 * `Set[T]` for immutable sets with element type `T`

src/permissions-exclusive.md

@@ -17,11 +17,7 @@ method exclusivity(x: Ref, y: Ref) {
 > * Add the third inhale statement `inhale x == y` anywhere before the exhale statement and change the latter to `exhale false`. Can false be asserted? Why does this demonstrate that it is not possible to hold more than one exclusive permission to `x.f`?
 
 In Viper, accessibility predicates can be conjoined via `&&`; the resulting assertion requires the _sum_ of the permissions required by its two conjuncts. Therefore, the two statements `inhale acc(x.f); inhale acc(y.f)` (semicolons are required in Viper only if statements are on the same line) are equivalent to the single statement `inhale acc(x.f) && acc(y.f)`. In both cases, the obtained permissions imply that `x` and `y` cannot be aliases.
-Intuitively, the statement `inhale acc(x.f) && acc(y.f)` can be understood as inhaling permission to `acc(x.f)`, and in *addition* to that, inhaling the permission to `acc(y.f)`. Technically, this conjunction between resource assertions is strongly related to the *separating conjunction* from [separation logic](https://link.springer.com/chapter/10.1007/3-540-44802-0_1); formal details of the connection (and how to encode standard separation logic into Viper) can be found in [this paper](https://lmcs.episciences.org/802).
-
-<!--**TODO: maybe consider also a link to wikipedia (for separation logic and separating conjunction), as suggested in one of the feedback e-mails **.-->
-
-<!--**TODO: We could add a note here that briefly states that a conjunction between non-resource assertions, or a resource and a non-resource assertion, is the usual boolean conjunction. However, my feeling is that such a note will be more confusing then helpful.** -->
+Intuitively, the statement `inhale acc(x.f) && acc(y.f)` can be understood as inhaling permission to `acc(x.f)`, and in *addition* to that, inhaling the permission to `acc(y.f)`. Technically, this conjunction between resource assertions is strongly related to the *separating conjunction* from [separation logic](https://link.springer.com/chapter/10.1007/3-540-44802-0_1) (see also the [Wikipedia article](https://en.wikipedia.org/wiki/Separation_logic)); formal details of the connection (and how to encode standard separation logic into Viper) can be found in [this paper](https://lmcs.episciences.org/802).
 
 We can now see how exclusive permissions enable framing and modular verification, as illustrated by the next example below. Here, method `client` is able to frame the property `b.f == 3` across the call to `inc(a, 3)` because holding permission to both `a.f` and `b.f` implies that `a` and `b` cannot be aliases, and because method `inc`'s specification states that `inc` only requires the permission to `a.f`. Since permission to `b.f` is _retained_, the value of `b.f` can be framed across the method call. Informally, and thinking more operationally, the method would not be able to modify this field location, since it lacks the necessary permission to do so.
 

src/permissions-fractional.md

@@ -73,3 +73,5 @@ method client(a: Ref, b: Ref) {
 > * Can you fix the new code by changing the specifications of method `copyAndInc`?
 > * Revert to the original example. Afterwards, modify method `client` as follows: change the invocation of method `copyAndInc` to `copyAndInc(a, a)`, and change the `assert` statement to `assert b.f == 3 && a.f == 2`. To verify the resulting code, you'll have to change the specifications of method `copyAndInc`.
 > * Can you find specifications for method `copyAndInc` that allow verifying both versions of method `client`: the original implementation (`copyAndInc(a, b); assert b.f == 3 && a.f == 4`) and the new one (`copyAndInc(a, a); assert b.f == 3 && a.f == 2`). That is, can you find specifications that work, regardless of whether or not the passed references are aliases?
+
+Note that permission amounts are interpreted differently in the preconditions of Viper *functions* (introduced [later in this tutorial](./functions.md)): since functions cannot modify the heap, only the distinction between zero and positive permission amounts matters there, and concrete permission amounts are ignored; see the [section on functions](./functions.md) for details.