Standard libraries #22

robin-aws · 2023-12-13T20:10:11Z

No description provided.

robin-aws · 2023-12-13T20:11:53Z

builders/pandoc-dafny

I experimented with this in the hopes I could use pandoc to get Dafny snippet highlighting, but haven't got it working yet: it seems to tag all the right code elements with the right classes, but doesn't emit any of the dynamically generated CSS anywhere for some reason.

MikaelMayer · 2023-12-13T20:16:38Z

_posts/2023-12-20-standard-libraries.markdown

+Or perhaps you were distracted by the `Std.Strings` module, where you might expect these utilities to live.
+But in Dafny, strings are really nothing more than sequences of characters:
+the type `string` is just an alias for `seq<char>`.
+This means many typical string operations are provided as general sequence operations instead.


That sounds like a design issue. Could we have a module Strings refines Seq so that we not only provide everything Seq provides, but it's discoverable and extensible? I see how methods such as ToUpperCase could be in such a module.

If you agree with this, you can just resolve this comment by cutting an appropriate issue.

I agree there's room for improvement here in some way, and I cut this issue with several thoughts that came up while writing this: dafny-lang/dafny#4878

MikaelMayer · 2023-12-13T20:35:59Z

_posts/2023-12-20-standard-libraries.markdown

+the execution of the function body will immediately stop,
+and that failure will become the result of the whole function.
+At this point we have a valid Dafny program, and the IDE should reward our hard work
+with [a festive green gutter](https://dafny.org/blog/2023/04/19/making-verification-compelling-visual-verification-feedback-for-dafny)


MikaelMayer · 2023-12-13T20:36:42Z

_posts/2023-12-20-standard-libraries.markdown

+Dafny actually **knows** that they return the indexes of elements that satisfy the "by" predicate,
+and therefore deduces that `[line[firstDigitIndex], line[lastDigitIndex]]`
+is a string that only contains digits.
+I don't know about you but I think that's super cool.


Oh yeah that's excellent to highlight!

MikaelMayer · 2023-12-13T20:40:44Z

_posts/2023-12-20-standard-libraries.markdown

+method ReadPuzzleInput() returns (input: Wrappers.Result<string, string>) {
+  var bytesAsBVs :- FileIO.ReadBytesFromFile("input.txt");
+
+  var bytes := seq(|bytesAsBVs|, i requires 0 <= i < |bytesAsBVs| => bytesAsBVs[i] as BoundedInts.uint8);


It's unfortunate we need to do this conversion. We ought to be able to just cast. Anyway.

Agreed, also noted in dafny-lang/dafny#4878

MikaelMayer · 2023-12-13T20:41:20Z

_posts/2023-12-20-standard-libraries.markdown

+A few notes:
+
+* The `UnicodeStringsWithUnicodeChar` module is named that way to emphasize that it is only
+  correct to use with the `--unicode-char:true` mode, which is [on by default in Dafny 4.x](https://dafny.org/blog/2023/03/03/dafny-4-released/#unicode-strings). 


Suggested change

correct to use with the `--unicode-char:true` mode, which is [on by default in Dafny 4.x](https://dafny.org/blog/2023/03/03/dafny-4-released/#unicode-strings).

correct to use with the `unicode-char=true` option, which is [on by default in Dafny 4.x](https://dafny.org/blog/2023/03/03/dafny-4-released/#unicode-strings).

Since you are using the dfyconfig.toml :-)

Good point - I think I'll call out the difference in syntax earlier and mention both forms here.

MikaelMayer · 2023-12-13T20:44:32Z

_posts/2023-12-20-standard-libraries.markdown

+in the main method than printing an error and exiting.
+`:- expect` means that if the right-hand side of the statement is a failure,
+Dafny will immediately halt and print the failure value to the console.
+This is particularly valuable for writing tests in Dafny.


I just discovered that tests can return failure-compatible types as well so you can use :- without expect. Not sure if it's worth mentioning here but perhaps in the future.

Indeed I'm still debating whether to frame the solution a little differently. As soon as I added the CI check of the solution I thought "this should really be a {:test} instead of a Main method". But on the other hand in the puzzle solving context you don't actually know the answer so you do need a Main method you just run as well, plus I feel like printing out the answer is just more exciting than a passing test case. :)

In fact I think I'll actually call this out explicitly and do both, since I'm already calling out similar Real Code issues outside of the puzzle context anyway.

MikaelMayer · 2023-12-13T20:44:54Z

_posts/2023-12-20-standard-libraries.markdown

+% dafny run dfyconfig.toml
+
+Dafny program verifier finished with 3 verified, 0 errors
+142


I got the same result too! good job :-)

MikaelMayer · 2023-12-13T20:45:30Z

_posts/2023-12-20-standard-libraries.markdown

+(see below for the complete program),
+all thanks to the Dafny standard libraries.
+
+```dafny


Can you use import statements like John's blog post, so that you can verify this piece of code?

I'm still trying to figure out the best way to do that and get nice syntax highlighting on the snippets. I'm not using Madoko and trying to find a more standard solution, hence experimenting with pandoc. My fallback approach will be to use the verification-compelling-verification-steps.js script and the {% include ... %} directives it supports, as the most recent post did.

I ended up switching to Madoko and just including the final solution source, so at least that is continuously checked. It didn't seem worth it to convert the other snippets to source since they aren't complicated, and some are not even expected to be valid since they are partial work-in-progress.

…ries # Conflicts: # Makefile

…ries

ssomayyajula

Looks good overall!

_posts/2023-12-20-standard-libraries.markdown

MikaelMayer

Only two comments! I loved the very casual introduction of this blog post and the fact that you made it entertaining throughout, with appropriate links and comments about anything readers might be wondering. Left me with a sense of happiness.

assets/mdk/standard-libraries.mdk

MikaelMayer · 2023-12-19T18:41:27Z

assets/mdk/standard-libraries.mdk

+in the main method than printing an error and exiting.
+`:- expect` means that if the right-hand side of the statement is a failure,
+Dafny will immediately halt and print the failure value to the console.
+This is particularly valuable for writing tests in Dafny.


Suggested change

This is particularly valuable for writing tests in Dafny.

This is particularly valuable for writing tests in Dafny, but don't use it in production code!

Or something similar implying that we should not use expect statements anywhere else normally. Not like Rust's unwrap for example.

That version is a bit strong but I pushed my own only slightly softer variation. :)

Co-authored-by: Mikaël Mayer <[email protected]>

robin-aws added 8 commits December 12, 2023 16:18

Experimenting with build

54d6d70

Lie about date for now

e290bd0

Fix source

81ddd10

Get some more libraries referenced :)

c2402c9

Partial work

157abbc

Complete core material

df7ad60

Remove pandoc experiments for now

e1acf45

Tweak title

94cca1a

robin-aws commented Dec 13, 2023

View reviewed changes

MikaelMayer reviewed Dec 13, 2023

View reviewed changes

robin-aws added 8 commits December 14, 2023 18:50

Flesh out front and back

5c72186

Merge branch 'main' of github.com:dafny-lang/blog into standard-libra…

e39f910

…ries # Conflicts: # Makefile

Missing file from last checkin 🤦

62507f2

Merge branch 'main' of github.com:dafny-lang/blog into standard-libra…

c094b87

…ries

Cleanup

d06391f

Switch to madoko just to get syntax highlighting

ba4ecd8

Include final snippet from source project at least

146badd

Last TODO and misc proof editing

48497f6

robin-aws marked this pull request as ready for review December 18, 2023 22:02

ssomayyajula self-requested a review December 19, 2023 16:46

ssomayyajula reviewed Dec 19, 2023

View reviewed changes

Add comments about type errors

5d69a76

MikaelMayer reviewed Dec 19, 2023

View reviewed changes

robin-aws and others added 2 commits December 19, 2023 11:12

Update assets/mdk/standard-libraries.mdk

8d10026

Co-authored-by: Mikaël Mayer <[email protected]>

Warning about expect

6e2d492

ssomayyajula approved these changes Dec 19, 2023

View reviewed changes

MikaelMayer approved these changes Dec 20, 2023

View reviewed changes

robin-aws merged commit 651a721 into main Dec 20, 2023
1 check passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Standard libraries #22

Standard libraries #22

robin-aws commented Dec 13, 2023

robin-aws Dec 13, 2023

MikaelMayer Dec 13, 2023

robin-aws Dec 13, 2023

MikaelMayer Dec 13, 2023

MikaelMayer Dec 13, 2023

MikaelMayer Dec 13, 2023

robin-aws Dec 13, 2023

MikaelMayer Dec 13, 2023

robin-aws Dec 13, 2023

MikaelMayer Dec 13, 2023

robin-aws Dec 13, 2023

MikaelMayer Dec 13, 2023

MikaelMayer Dec 13, 2023

robin-aws Dec 13, 2023

robin-aws Dec 18, 2023

ssomayyajula left a comment

MikaelMayer left a comment

MikaelMayer Dec 19, 2023

robin-aws Dec 19, 2023

	correct to use with the `--unicode-char:true` mode, which is [on by default in Dafny 4.x](https://dafny.org/blog/2023/03/03/dafny-4-released/#unicode-strings).
	correct to use with the `unicode-char=true` option, which is [on by default in Dafny 4.x](https://dafny.org/blog/2023/03/03/dafny-4-released/#unicode-strings).

	This is particularly valuable for writing tests in Dafny.
	This is particularly valuable for writing tests in Dafny, but don't use it in production code!

Standard libraries #22

Standard libraries #22

Conversation

robin-aws commented Dec 13, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ssomayyajula left a comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment