-
Notifications
You must be signed in to change notification settings - Fork 260
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Documentation of nameonly and default values for formals #3903
Changes from 4 commits
87ef620
2f633cc
13a17d8
5127a5c
e9859e9
83ca44a
f61f9f5
3e0e351
68de8fd
35badc7
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -1886,7 +1886,7 @@ Furthermore, for the compiler to be able to make an appropriate choice of | |
representation, the constants in the defining expression as shown above must be | ||
known constants at compile-time. They need not be numeric literals; combinations | ||
of basic operations and symbolic constants are also allowed as described | ||
in [Section 9.38](#sec-compile-time-constants). | ||
in [Section 9.37](#sec-compile-time-constants). | ||
|
||
### 5.7.1. Conversion operations {#sec-conversion} | ||
|
||
|
@@ -4502,4 +4502,65 @@ imposed on the body of `ReachableVia` makes sure that, if the | |
predicate returns `true`, then every object reference in `p` is as old | ||
as some object reference in another parameter to the predicate. | ||
|
||
## 6.5. Nameonly Formal Parameters and Default-Value Expressions | ||
|
||
A formal parametes of a method, constructor in a class, iterator, | ||
function, or datatype constructor can be declared with an expression | ||
denoting a _default value_. This makes the parameter _optional_, | ||
as opposed to _required_. All required parameters must be declared | ||
before any optional parameters. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. No, this is no longer true (once #3864 is merged). A required parameter is allowed to follow an optional parameter, provided the required parameter is Actually, L4538 says what needs to be said. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Removed the sentence. |
||
|
||
For example, | ||
<!-- %check-resolve %save f.tmp --> | ||
```dafny | ||
function f(x: int, y: int := 10): int | ||
``` | ||
may be called as either | ||
<!-- %check-resolve %use f.tmp --> | ||
```dafny | ||
const i := f(1,2); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add space after There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. OK |
||
const j := f(1); | ||
``` | ||
where `f(1)` is equivalent to `f(1,10)` in this case. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add space after There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. OK |
||
|
||
Formal parameters may also be declared `nameonly`, in which case a call site | ||
must explicitly name the formal when providing its actual argument. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think it would be nicer to explain There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done |
||
|
||
The above function may be called as | ||
<!-- %no-check --> | ||
```dafny | ||
var k := f(y:=10, x:=2); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add a space on both sides of There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Done |
||
``` | ||
using names; here, though there are no `nameonly` parameters so the names may be used | ||
or the actual arguments may be given in order. | ||
|
||
If a function is declared with a `nameonly` formal, then that formal's value must be given with a named assignment. | ||
For example, a function `ff` declared as | ||
<!-- %check-resolve --> | ||
```dafny | ||
function ff(x: int, nameonly y: int): int | ||
``` | ||
may be called only using `ff(0, y := 4)`. A `nameonly` formal may also have a default value and thus be optional. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. "only" here feels a bit confusing. For one, the parameters don't have to be passed in as There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Right. Fixed. |
||
|
||
Any formals after a `nameonly` formal must either be `nameonly` themselves or have default values. | ||
Otherwise an error will result when an attempt is made to call the function or method with such a formal list. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. L4539 describes the motivation for L4538, from the language-design perspective. If L4538 is violated, Dafny will give an error for the declaration of the formals, so what happens at a call site is a moot point. I suggest keeping just L4538 and deleting L4539. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. In this code
Dafny gives an error on the const declaration, but not on the function. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Apparently, this has been fixed since Dafny 4.0. We now get an error on the function declaration as well. |
||
|
||
The formals of datatype constructors are not required to have names. Such formals may have default values but | ||
may not be declared `nameonly`. Such nameless formals must be declared before `nameonly` formals. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. No, a nameless formal is neither allowed to have a default value nor allowed to be declared There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. OK, but I would think a default value for a nameless formal to be a perfectly reasonable thing. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I agree. It would be a perfectly reasonable thing. We could add it in the future. |
||
|
||
The default-value expression for a parameter is allowed to mention the | ||
other parameters, including `this` (for instance methods and instance | ||
functions), but not the implicit `_k` parameter in least and greatest | ||
predicates and lemmas. The default value of a parameter may mention | ||
both preceding and subsequent parameters, but there may not be any | ||
dependent cycle between the parameters and their default-value | ||
expressions. | ||
|
||
The well-formedness of default-value expressions is checked independent | ||
of the precondition of the enclosing declaration. For a function, the | ||
parameter default-value expressions may only read what the function's | ||
`reads` clause allows. For a datatype constructor, parameter default-value | ||
expressions may not read anything. A default-value expression may not be | ||
involved in any recursive or mutually recursive calls with the enclosing | ||
declaration. | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since this paragraph explains "effectively nameonly", you may want to add a similar paragraph that explains "effectively required" (see #3864).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually, I found the 'effectively' terminology unhelpful -- better is simply stating and enforcing the rules about which formals can be optional and which can be nameonly.