diff --git a/text/0000-final-parameter.md b/text/0000-final-parameter.md new file mode 100644 index 0000000..5979a25 --- /dev/null +++ b/text/0000-final-parameter.md @@ -0,0 +1,192 @@ +- Feature Name: `final_parameters` +- Start Date: `17-10-2017` +- RFC PR: (leave this empty) +- See Also: [RFC#0005](https://github.com/Whiley/RFCs/blob/master/text/0005-final-modifier.md) + +# Summary + +Parameters in Whiley are currently treated in the same fashion as +local variables, meaning they can be assigned within the body of a +function or method. Unfortunately, this results in some potential +confusion when it comes to interpreting `ensures` clauses. To prevent +such confusion, this proposal is to require that parameters are +`final` by default. + +# Motivation + +Parameters in Whiley are mutable and can be assigned within the body +of a function or method. Unfortunately, this causes confusion over +the meaning of a parameter used in an `ensures` clause. The following +illustrates: + +``` +function abs(int x) -> (int r) +ensures r >= 0 +ensures (r == x) || (r == -x): + // + if x < 0: + x = -x + return x +``` + +The issue here is that the `ensures` clause refers to the value of `x` +as it was on entry to the function, rather than its value at the end. +This is potentially confusing (e.g. for students) since `r==x` would +appear to always hold at the `return` statement. + +We can make an interesting generalisation here which further +illustrates the problem. Specifically this code: + +``` +function f(int x) -> (int r) +requires P +ensures Q: + BODY + return E +``` + +where `E` is some expression, might (in some sense) be considered +equivalent to this: + +``` +function f(int x) -> (int r): + assume P + BODY + assert Q[E/r] + return E +``` + +But, this equivalence does not hold if `x` is allowed to change within +the body of the function. + +## Solution + +The proposed solution is fairly straightforward. We simply treat +parameters as `final` by default, thereby preventing assignment to +them within the body of a function or method. Thus, our `abs()` +method above would fail compilation with an error such as the +following: + +``` +abs.whiley:6: assignment to parameter not permitted + x = -x + ^^^^^^ +``` + +We note that the Dafny language also does not permit assignment to +parameters, and it may be this is the reason why. + +The implementation of this proposal is relatively straightforward and +employs an algorithm for _definite unassignment_ (see below). + +## Implications + +There are a number of interesting effects from this proposal (aside +from the potential for widespread code breakage): + +**Heap Versioning Syntax.** An important question is the syntax for + expressing the _before_ and _after_ effects of a method on the heap. + For example, + [WyC#750](https://github.com/Whiley/WhileyCompiler/issues/750) uses + this example to illustrate: + +``` +method swap(&int x, &int y) +ensures *x == *'y && *y == *'x: + int tmp = *x + *x = *y + *y = tmp +``` + +Here, `*'` was intended to be read as: _the state of the heap at the +point of completion_. Thus, `*'x` is here denoting the value of the +location referred to by `x` _after the method completes_. + +This proposal suggests an alternative interpretation of `*'` would be +sensible. Specifically, following the above interpretation and our +equivalence from before, we end up with: + + +``` +method swap(&int x, &int y): + int tmp = *x + *x = *y + *y = tmp + assert (*x == *'y) && (*y == *'x) +``` + +Here, it makes much more sense for `*x` to refer to the current value, +and `*'x` to refer to the original value. This would then be +comparable to the `\old()` syntax used in JML and the `old()` notation +used in Dafny. + +**Cloning.** As discussed in + [RFC#0005](https://github.com/Whiley/RFCs/blob/master/text/0005-final-modifier.md) + there are some potential benefits from `final` parameters in the + context of value semantics. The minimal example is this: + +``` +function f(int[] xs) -> (int r): + return |xs| + +function g(int[] xs) -> (int r): + ... + int x = f(xs) + ... + return x + ``` + +At the point of the function invocation, the compiler must determine +whether or not to clone the array `xs`. In doing this, the compiler +can only use the function's signature (i.e. name, parameter types and +requires / ensures clauses). In deciding whether to clone `xs` above, +the compiler can consider the remainder of the function body. There +are two cases: either `xs` is used after the inovcation; or, it is +not. If `xs` is not used after the invocation then it does not need to +be cloned. However, if `xs` is used after the invocation then the +compiler has no choice and must clone `xs`. This would be unfortunate +in this case as the clone was unnecessary (i.e. because `xs` is not +assigned within the body of `f()`). Note, however, that under this +proposal `xs` would be a `final` variable and, hence, the compiler +would know that it could not be assigned within the body of the +invoked function. + +**Shadow variables.** When generating code with the intention of + performing runtime assertion checking, the compiler currently must + insert so-called _shadow variables_ to hold the values of parameters + on entry to the function/method. This is necessary to that they can + be restored before evaluating the postcondition at the point of a + `return`. Under this proposal, shadow variables become unnecessary + because parameters cannot be modified. + +# Technical Details + +Definite unassignment is the process of checking that a variable is +not assigned again within the body of a function or method. This is +typically implemented as a dataflow analysis, and was perhaps first +introduced in +[Java](https://docs.oracle.com/javase/specs/jls/se7/html/jls-16.html). + +The implementation of this proposal employs a simplified version of +the _definite unassignment_ algorithm described in +[RFC#0005](https://github.com/Whiley/RFCs/blob/master/text/0005-final-modifier.md). +It is a simplification because we do not need to consider variables +(i.e. parameters) which are not initialised. + +# Terminology + +* **Definite Unassignment Analysis**. This is the process of checking + that a variable marked final is never assigned after initialisation. + +# Drawbacks and Limitations + +The drawbacks are relatively obvious. All existing code may suffer +breakage as a result of this proposal. This includes code in +benchmark suites, test suites, published papers, student assignments, +the Whiley Language Specification, the Whiley Standard Library. In +short, it is potentially a significant cost to update all of this +existing code. + +# Unresolved Issues + +None.