Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Generate constructors with default assignments to non-required fields #133

Open
codyroux opened this issue Feb 6, 2023 · 4 comments
Open

Generate constructors with default assignments to non-required fields #133

codyroux opened this issue Feb 6, 2023 · 4 comments
Assignees
@alex-chew
Labels
general-dafny-use New functionality or clean up for broader use of this repo going-public Should be done before launching 0.x publicly Needs Tests This feature may have been implemented, but lacks sufficient test coverage.
Milestone
Public 0.x launch

Comments

@codyroux
Copy link
Collaborator

codyroux commented Feb 6, 2023

The title sums it up: assigning None to non-required fields by default would avoid some pain when actually creating members of these records. I think this is the relevant Dafny section: https://dafny.org/dafny/DafnyRef/DafnyRef#2146-formal-parameters-and-default-value-expressions
@robin-aws
Copy link
Contributor

I'm surprised this hasn't already caused trouble for existing projects. There are a lot of changes in Smithy 2.0 related to default values that might give the right answer for members in general.

@robin-aws robin-aws added the general-dafny-use New functionality or clean up for broader use of this repo label Mar 1, 2023
@robin-aws
Copy link
Contributor

This is actually necessary to implement the Smithy specification correctly: without default values, adding another member to an input structure will break existing Dafny code.

@robin-aws robin-aws added the going-public Should be done before launching 0.x publicly label May 3, 2023
@robin-aws robin-aws self-assigned this May 3, 2023
@alex-chew alex-chew assigned alex-chew and unassigned robin-aws May 3, 2023
@alex-chew alex-chew self-assigned this May 3, 2023
@seebees
Copy link
Contributor

seebees commented May 4, 2023

This has to wait for Dafny 4.1
dafny-lang/dafny#3864

@texastony texastony mentioned this issue Dec 4, 2023
Merged
@ajewellamz ajewellamz added the Needs Tests This feature may have been implemented, but lacks sufficient test coverage. label Dec 4, 2023
@ajewellamz
Copy link
Contributor

Fixed. #305
Leaving this open, because it needs coverage in a Test Model.

robin-aws pushed a commit that referenced this issue Apr 19, 2024
@seebees
Add back benerated information (#133)
c35d027
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@alex-chew alex-chew

Labels
general-dafny-use New functionality or clean up for broader use of this repo going-public Should be done before launching 0.x publicly Needs Tests This feature may have been implemented, but lacks sufficient test coverage.
Projects
None yet
Milestone
Public 0.x launch
Development

No branches or pull requests
5 participants
@seebees @codyroux @alex-chew @robin-aws @ajewellamz