From 87ef620a2a59088f1349e58b8fdc275da904409e Mon Sep 17 00:00:00 2001 From: davidcok Date: Sat, 22 Apr 2023 22:22:17 -0400 Subject: [PATCH 1/5] RM edits for nameonly and default values: --- docs/DafnyRef/Expressions.md | 44 +++++++++++---------------- docs/DafnyRef/Types.md | 59 +++++++++++++++++++++++++++++++++++- 2 files changed, 75 insertions(+), 28 deletions(-) diff --git a/docs/DafnyRef/Expressions.md b/docs/DafnyRef/Expressions.md index 0d20fa9c145..07adf0ca314 100644 --- a/docs/DafnyRef/Expressions.md +++ b/docs/DafnyRef/Expressions.md @@ -1825,6 +1825,21 @@ Method calls, object-allocation calls (`new`), function calls, and datatype constructors can be called with both positional arguments and named arguments. +Formal parameters have three ways to indicate how they are to be passed in: +- nameonly: the only way to give a specific argument value is to name the parameter +- positional only: these are nameless parameters (which are allowed only for datatype constructor parameters) +- either positional or by name: this is the most common parameter + +A parameter is either required or optional: +- required: a caller has to supply an argument +- optional: the parameter has a default value that is used if a caller omits passing a specific argument + +The syntax for giving a positional-only (i.e., nameless) parameter does not allow a default-value expression, so a positional-only parameter is always required. + +At a call site, positional arguments are not allowed to follow named arguments. Therefore, if `x` is a nameonly parameter, then there is no way to supply the parameters after `x` by position. +Thus, any parameter that follows `x` must either by passed by name or have a default value. +That is, if a later (in the formal parameter declaration) parameter does not have a default value, it is effectively nameonly. + Positional arguments must be given before any named arguments. Positional arguments are passed to the formals in the corresponding position. Named arguments are passed to the formal of the given @@ -1837,32 +1852,7 @@ value for each optional parameter, and must never name non-existent formals. Any optional parameter that is not given a value takes on the default value declared in the callee for that optional parameter. -## 9.37. Formal Parameters and Default-Value Expressions - -The formal parameters 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. All nameless parameters in a datatype -constructor must be declared before any `nameonly` parameters. - -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. - -## 9.38. Compile-Time Constants {#sec-compile-time-constants} +## 9.37. Compile-Time Constants {#sec-compile-time-constants} In certain situations in Dafny it is helpful to know what the value of a constant is during program analysis, before verification or execution takes @@ -1903,7 +1893,7 @@ In Dafny, the following expressions are compile-time constants[^CTC], recursivel [^CTC]: This set of operations that are constant-folded may be enlarged in future versions of `dafny`. -## 9.39. List of specification expressions {#sec-list-of-specification-expressions} +## 9.38. List of specification expressions {#sec-list-of-specification-expressions} The following is a list of expressions that can only appear in specification contexts or in ghost blocks. diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index 1c7db30d055..51e8af88dde 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -1879,7 +1879,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} @@ -4495,4 +4495,61 @@ 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 + +The formal parameters 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. + +For example, +``` +function f(x: int, y: int := 10): int +``` +may be called as either +``` +var i := f(1,2); +var j := f(1); +``` +where `f(1)` is equivalent to `f(1,10)` in this case. + +Formal parameters may also be declared `nameonly`, in which case a call site +must explicitly name the formal when providing its actual argument. + +The above function may be called as +``` +var k := f(y:=10, x:=2); +``` +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 +``` +function ff(x: int, nameonly y: int) +``` +may be called only using `ff(0, y := 4)`. A `nameonly` formal may also have a default value and thus be optional. + +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. + +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. + +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. From 2f633cc3a65c94b76606eda7533a36079db5cfe3 Mon Sep 17 00:00:00 2001 From: davidcok Date: Mon, 24 Apr 2023 07:46:32 -0400 Subject: [PATCH 2/5] Minor edit --- docs/DafnyRef/Types.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index 51e8af88dde..aa1e8fd7498 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -4497,7 +4497,7 @@ as some object reference in another parameter to the predicate. ## 6.5. Nameonly Formal Parameters and Default-Value Expressions -The formal parameters of a method, constructor in a class, iterator, +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 @@ -4531,7 +4531,7 @@ function ff(x: int, nameonly y: int) ``` may be called only using `ff(0, y := 4)`. A `nameonly` formal may also have a default value and thus be optional. -Any formals after a nameonly formal must either be nameonly themselves or have default values. +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. The formals of datatype constructors are not required to have names. Such formals may have default values but From 13a17d886d116dc89f98d5b51dec6ec3cee4fadc Mon Sep 17 00:00:00 2001 From: davidcok Date: Mon, 24 Apr 2023 08:42:29 -0400 Subject: [PATCH 3/5] Fixing examples --- docs/DafnyRef/Types.md | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index aa1e8fd7498..e6a0dcd3637 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -4504,13 +4504,15 @@ as opposed to _required_. All required parameters must be declared before any optional parameters. For example, -``` + +```dafny function f(x: int, y: int := 10): int ``` may be called as either -``` -var i := f(1,2); -var j := f(1); + +```dafny +const i := f(1,2); +const j := f(1); ``` where `f(1)` is equivalent to `f(1,10)` in this case. @@ -4518,7 +4520,8 @@ Formal parameters may also be declared `nameonly`, in which case a call site must explicitly name the formal when providing its actual argument. The above function may be called as -``` + +```dafny var k := f(y:=10, x:=2); ``` using names; here, though there are no `nameonly` parameters so the names may be used @@ -4526,8 +4529,9 @@ 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 -``` -function ff(x: int, nameonly y: int) + +```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. From e9859e9332b7ec5f6f4e65c6894e22c7c3e96e89 Mon Sep 17 00:00:00 2001 From: davidcok Date: Mon, 24 Apr 2023 19:50:54 -0400 Subject: [PATCH 4/5] Review edits --- docs/DafnyRef/Expressions.md | 2 +- docs/DafnyRef/Types.md | 33 +++++++++++++++++---------------- 2 files changed, 18 insertions(+), 17 deletions(-) diff --git a/docs/DafnyRef/Expressions.md b/docs/DafnyRef/Expressions.md index 07adf0ca314..839aa9fae39 100644 --- a/docs/DafnyRef/Expressions.md +++ b/docs/DafnyRef/Expressions.md @@ -1837,7 +1837,7 @@ A parameter is either required or optional: The syntax for giving a positional-only (i.e., nameless) parameter does not allow a default-value expression, so a positional-only parameter is always required. At a call site, positional arguments are not allowed to follow named arguments. Therefore, if `x` is a nameonly parameter, then there is no way to supply the parameters after `x` by position. -Thus, any parameter that follows `x` must either by passed by name or have a default value. +Thus, any parameter that follows `x` must either be passed by name or have a default value. That is, if a later (in the formal parameter declaration) parameter does not have a default value, it is effectively nameonly. Positional arguments must be given before any named arguments. diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index e6a0dcd3637..7c5927b5180 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -4497,11 +4497,10 @@ 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, +A formal parameter 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. +as opposed to _required_. For example, @@ -4511,35 +4510,37 @@ function f(x: int, y: int := 10): int may be called as either ```dafny -const i := f(1,2); +const i := f(1, 2); const j := f(1); ``` -where `f(1)` is equivalent to `f(1,10)` in this case. +where `f(1)` is equivalent to `f(1, 10)` in this case. -Formal parameters may also be declared `nameonly`, in which case a call site -must explicitly name the formal when providing its actual argument. - -The above function may be called as +The above function may also be called as ```dafny -var k := f(y:=10, x:=2); +var k := f(y := 10, x := 2); ``` -using names; here, though there are no `nameonly` parameters so the names may be used -or the actual arguments may be given in order. +using names; actual arguments with names may be given in any order, +though they must be after actual arguments without names. + +Formal parameters may also be declared `nameonly`, in which case a call site +must always explicitly name the formal when providing its actual argument. -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 ```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. +must be called either by listing the value for x and then y with a name, +as in `ff(0, y := 4)` or by giving both actuals by name (in any order). +A `nameonly` formal may also have a default value and thus be optional. 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. -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. +The formals of datatype constructors are not required to have names. +A nameless formal may not have a default value, nor may it follow a formal +that has a default value. The default-value expression for a parameter is allowed to mention the other parameters, including `this` (for instance methods and instance From f61f9f567a4b538c7776bec2cd28ad7b8363ca3c Mon Sep 17 00:00:00 2001 From: davidcok Date: Mon, 24 Apr 2023 19:53:55 -0400 Subject: [PATCH 5/5] One more repair --- docs/DafnyRef/Types.md | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index 8c5f4d719d6..5422d53bbae 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -4543,7 +4543,6 @@ as in `ff(0, y := 4)` or by giving both actuals by name (in any order). A `nameonly` formal may also have a default value and thus be optional. 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. The formals of datatype constructors are not required to have names. A nameless formal may not have a default value, nor may it follow a formal