Miscellaneous edits to the new library, to support testing (#117)

* Working on reusable tests * Debugging * Debugging #2 * Debugging #3 * Debugging #4 * Debugging #4 * Debugging #5 * Debugging #6 * Debugging #7 * Debugging #8 * Debugging #9 * Debugging #10 * Debugging #11 * Debugging #12 * Debugging #13 * Debugging #14 * Debugging #14 * Debugging * Debugging * Debugging * Debugging * OK, except disabling 3.13.1 and nightly-latest until setup-dafny-action is fixed * OK, except disabling 3.13.1 and nightly-latest until setup-dafny-action is fixed * Fixing the concurrency check * Old edits * Edits to examples * Touchups to examples and library * Math relations and examples * Some docstring documentation * Some docstring documentation * typo * Formatting * Removing semicolon * Adjusting for Dafny 3 * Attempt to fix proof in ld dafny versions * Fixing up docstrings * Fixed examples * Fixed formatting * Fixed formatting * Formatting * Formatting --------- Co-authored-by: davidcok <[email protected]>
dafny-lang · Apr 17, 2023 · 7c386fa · 7c386fa
1 parent b0c15d0
commit 7c386fa
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 6 deletions.
diff --git a/src/dafny/BinaryOperations.dfy b/src/dafny/BinaryOperations.dfy
@@ -5,7 +5,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} BinaryOperations {
+/** Defines a number of (ghost) properties of binary operations */
+module {:options "-functionSyntax:4"} BinaryOperations
+{
 
   ghost predicate IsAssociative<T(!new)>(bop: (T, T) -> T) {
     forall x, y, z :: bop(bop(x, y), z) == bop(x, bop(y, z))

diff --git a/src/dafny/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy b/src/dafny/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy
@@ -8,7 +8,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Dafny.DivInternalsNonlinear {
+/** Declares a few helper lemmas for internal use in non-linear arithmetic */
+module {:options "-functionSyntax:4"} Dafny.DivInternalsNonlinear
+{
 
   /* WARNING: Think three times before adding to this file, as nonlinear
   verification is highly unstable! */

diff --git a/src/dafny/NonlinearArithmetic/Internals/GeneralInternals.dfy b/src/dafny/NonlinearArithmetic/Internals/GeneralInternals.dfy
@@ -8,7 +8,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Dafny.GeneralInternals {
+/** Declares helper lemmas and predicates for non-linear arithmetic */
+module {:options "-functionSyntax:4"} Dafny.GeneralInternals
+{
 
   /* this predicate is primarily used as a trigger */
   ghost predicate IsLe(x: int, y: int)

diff --git a/src/dafny/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy b/src/dafny/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy
@@ -8,7 +8,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Dafny.ModInternalsNonlinear {
+/** Declares helper lemmas about the mod operation */
+module {:options "-functionSyntax:4"} Dafny.ModInternalsNonlinear
+{
 
   /* WARNING: Think three times before adding to this file, as nonlinear
   verification is highly unstable! */

diff --git a/src/dafny/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy b/src/dafny/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy
@@ -8,7 +8,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Dafny.MulInternalsNonlinear {
+/** Declares some helper lemmas about multiply, for internal use */
+module {:options "-functionSyntax:4"} Dafny.MulInternalsNonlinear
+{
 
   /* WARNING: Think three times before adding to this file, as nonlinear
   verification is highly unstable! */

diff --git a/src/dafny/Unicode/Utf8EncodingForm.dfy b/src/dafny/Unicode/Utf8EncodingForm.dfy
@@ -13,7 +13,7 @@ include "UnicodeEncodingForm.dfy"
 
 /**
   * The Unicode encoding form that assigns each Unicode scalar value to an unsigned byte sequence of one to four bytes
-  * in length, as specified in Table 3-6 and Table 3-7.
+  * in length, as specified in Table 3-6 and Table 3-7 of the Unicode Standard, Version 14.0.
   */
 module {:options "-functionSyntax:4"} Dafny.Utf8EncodingForm refines UnicodeEncodingForm {
   type CodeUnit = bv8