Documentation for the library #100

davidcok · 2023-02-23T17:44:31Z

Just the docs.

robin-aws

Wonderful to have so much more documentation on this code, thank you. There are some lingering pieces of #92 in here still - while you're addressing those I'll go review that PR so I have more context in case that helps.

robin-aws · 2023-02-23T18:26:21Z

src/dafny/BoundedInts.md

+- unsigned types of 8, 16, 32, 64, 128 bit widths (e.g. `uint32`)
+- signed types of 8, 16, 32, 64, 128 bit widths (e.g. `int16`)


Suggested change

- unsigned types of 8, 16, 32, 64, 128 bit widths (e.g. `uint32`)

- signed types of 8, 16, 32, 64, 128 bit widths (e.g. `int16`)

- unsigned types of 8, 16, 32, 64 bit widths (e.g. `uint32`)

- signed types of 8, 16, 32, 64 bit widths (e.g. `int16`)

robin-aws · 2023-02-23T18:26:56Z

src/dafny/BoundedInts.md

+Dafny itself generally uses and reasons about mathematical, unbounded integers and natural numbers.
+However compiled programs, for efficiency of computation and storage, will generally use fixed-bit-width
+numbers. So Dafny defines them here, for use when needed.
+
+An important implementation point about these type definitions is Dafny can determine which native type 
+in the target compiled program best matches the Dafny type. For example, the Dafny type `int16` is
+a signed integer that fits in 16 bits. If a program using this type is compiled to, say Java, then
+variables of this Dafny type will be compiled to Java `short` variables. In some cases there is no
+natural match. For example Java does not have an unsigned 16-bit type while C# and C++ do.


YES, thank you! This is worth documenting somewhere with very high visibility in the reference manual/user guide as well.

src/dafny/BoundedInts.md

robin-aws · 2023-02-23T18:28:46Z

src/dafny/BoundedInts.md

+In addition, the module defines a number of constants that are powers of two (not all of them, just those that are generally useful).
+They are useful in stating the ranges of fixed-bit-width integers. Examples are `TWO_TO_THE_15`, `TWO_TO_THE_32`.
+
+Here are two example methods. In the first, the module `Dafny.BoundedInts` is renamed to `T`, which is then used as the prefix for type and constant names.


nit: in my experience T is much more often a type parameter than a module alias. Perhaps BI instead?

OK- changed

robin-aws · 2023-02-23T18:31:40Z

src/dafny/BoundedInts.md

+
+Here are two example methods. In the first, the module `Dafny.BoundedInts` is renamed to `T`, which is then used as the prefix for type and constant names.
+In the second, the module is imported as opened, in which case the type and constant names can be used without qualification.
+<!-- %check-verify -->


This repo doesn't check these inline directives does it? We should either move these examples under examples or add that automation.

I think my preference would be the latter, mirroring the way most Dafny projects will define tests/examples, rather than how we do it in the reference manual. But it's worth thinking about supporting something like Python's doctests in Dafny too in the future.

No it doesn't, but that is a one-line change in doc-tests.yml (in the dafny repo testing) to turn on such checking once this PR is merged.

That's the wrong place to test changes to this repo's contents though. Would it be easy to set up the same checking here instead?

(and fine to add that later if so)

Yes - In the process of adapting the code to do that. We'll get it working in a subsequent PR.

robin-aws · 2023-02-23T18:43:28Z

src/dafny/Relations.md

+
+These properties are sometimes required for other functions. For example, 
+if one wants to sort a sequence by some relation `R`, one must establish that `R` is a _Total Ordering_. 
+In fact, that is part of the precondition of the sorting function.


This is slightly tricky since the one sorting function we have (Arrays.BinarySearch) requires a strict total ordering, but #57 will require a total ordering. Ideally we'd clean that up without breaking people, but for now the line above should probably say "Strict Total Ordering" instead.

robin-aws · 2023-02-23T18:44:35Z

src/dafny/Relations.md

+As a simple example, you might define a predicate like this:
+```dafny
+  const IntLT  := ((i: int, j: int) => (i < j))
+```
+
+and then need to proof this lemma to use it in a sorting routine:
+```dafny
+  lemma IntLTisStrictTotalOrder()
+    ensures StrictTotalOrdering(IntLT) {}
+```


Again better to only have under examples - perhaps add the content here as comments there instead?

Other reviewers (of other documentation) have predominantly preferred having examples directly present, both for reading and reviewing. I'll add the annotation to be sure these are checked in place.

Sure, as above I could see steering this repo towards having all inline examples instead of the current setup, and IF it is possible to set up the mechanism to test them I'm happy with that.

It is possible -- just like it is already in the other repo. But it has to be checked in and next to the new code.
Then I'll be able to create a yml to do the checking regularly or on demand.

robin-aws · 2023-02-23T18:49:56Z

src/dafny/Results.md

+
+### Combining different FC-types in methods
+
+_This is an experimental, tentatively planned, not yet implemented feature._


Move this content to an issue then please. We shouldn't be documenting potential ideas in the same place as what users can actually use.

Although I don't actually see the feature defined below, so I don't know if you need this warning anyway?

Correct - that line should have gone out when the workaround description came in.

src/dafny/Unicode/Unicode.md

robin-aws · 2023-02-23T18:50:48Z

src/dafny/Results.md

@@ -0,0 +1,178 @@
+
+## The `Results` module {#sec-results}


Nope I don't like burying Option under the label "Results" when it's not just used for that. Let's keep the term "Wrappers" in this PR and we can argue more about this in #92 :)

OK. Though this was the name Ryan suggested.

Co-authored-by: Robin Salkeld <[email protected]>

davidcok added 2 commits February 23, 2023 12:42

Just the docs

a19e5e0

Just the docs

b655573

robin-aws requested changes Feb 23, 2023

View reviewed changes

Update src/dafny/BoundedInts.md

cadcc13

Co-authored-by: Robin Salkeld <[email protected]>

davidcok closed this Mar 8, 2023

davidcok deleted the cok-docs3 branch March 8, 2023 15:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Documentation for the library #100

Documentation for the library #100

davidcok commented Feb 23, 2023

robin-aws left a comment

robin-aws Feb 23, 2023

robin-aws Feb 23, 2023

davidcok Feb 23, 2023

robin-aws Feb 23, 2023

davidcok Feb 23, 2023

robin-aws Feb 23, 2023

davidcok Feb 23, 2023

robin-aws Feb 23, 2023

robin-aws Feb 23, 2023

davidcok Feb 24, 2023

robin-aws Feb 23, 2023

davidcok Feb 23, 2023

robin-aws Feb 23, 2023

davidcok Feb 23, 2023

robin-aws Feb 23, 2023

davidcok Feb 24, 2023

robin-aws Feb 23, 2023

davidcok Feb 23, 2023

davidcok Feb 23, 2023

robin-aws Feb 23, 2023

davidcok Feb 23, 2023

		- unsigned types of 8, 16, 32, 64, 128 bit widths (e.g. `uint32`)
		- signed types of 8, 16, 32, 64, 128 bit widths (e.g. `int16`)


		### Combining different FC-types in methods

		_This is an experimental, tentatively planned, not yet implemented feature._

Documentation for the library #100

Documentation for the library #100

Conversation

davidcok commented Feb 23, 2023

robin-aws left a 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

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