From 21f48d3a3171930f497f222d9f85b42eccf027b4 Mon Sep 17 00:00:00 2001
From: John Tristan <trjohnb@amazon.com>
Date: Fri, 29 Sep 2023 09:26:32 -0400
Subject: [PATCH] Refined guidelines (#62)

Refining the guidelines

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---
 Guidelines.md | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/Guidelines.md b/Guidelines.md
index d98438ae..b6fe4587 100644
--- a/Guidelines.md
+++ b/Guidelines.md
@@ -1,4 +1,8 @@
-Following are guidelines that one should follow unless there is a good technical reason not to.
+The Dafny 386 guidelines.
+
+By default, you should adhere the following guidelines to structure your development. 
+It may happen that not following the guidelines would lead to a better solution: when that is
+the case, you should present your case with the rest of the developers. 
 
 * Languages features to avoid:
     * import opened.
@@ -8,10 +12,13 @@ Following are guidelines that one should follow unless there is a good technical
 
 * Even if a function is not meant to be part of the compiled code, don't use ghost unless necessary.
 * Do not attach postconditions to functions. Instead, prove the postcondition as a separate lemma.
+* Use function preconditions only when the function is genuinely partial and that making total would requires the use of the error monad or a dummy value.
 * Make functions opaque.
 * Name preconditions of lemmas and reveal them only when necessary.
 * Be mindful of resource usage and refine your proof until it is less than 1M.
-* In particular, avoid `{:vcs_split_on_every_assert}` as this can increase the verification time a lot.
+* Do not use internal prover directives such as `{:vcs_split_on_every_assert}` or `{:trigger}`.
+* A method should have a unique postcondition that establishes its equivalence with a functional model.
+* Local variables must be typed explicitly. 
 * Keep proofs short and modular, as for a pencil and paper proof.
 * Prefer structured proofs in natural deduction rathen than sequences of assertions.
 * Unless it is logically or mathematically necessary:
@@ -143,6 +150,7 @@ lemma Foo2()
       </td>
    </tr>
 </table>
+
 * Establish preconditions of assertion in a by clause. For example, consider lemma Foo() requires A ensures B
 <table>
    <tr>