Update prompts

prompts/dafny_eval/ask_for_fixed.txt

@@ -0,0 +1,5 @@
+This answer got Dafny verification error:
+{error}
+Please try again by taking the Dafny feedback.
+
+If an error appears in one of method ending with `_valid`, that means annotations of an existing function were altered.

prompts/dafny_eval/rewrite.txt

@@ -0,0 +1,6 @@
+Given a Dafny program with function signature, preconditions, postconditions, and code, but with annotations missing.
+Please return a complete Dafny program with the strongest possible annotations (loop invariants, assert statements, etc.) filled back in.
+Do not explain.
+Please use exactly the same function signature, preconditions, and postconditions. Do not ever modify the given lines.
+Below is the program:
+{program}

prompts/dafny_eval/sys.txt

@@ -0,0 +1,3 @@
+You are an expert in Dafny.
+You will be given tasks dealing with Dafny programs including precise annotations.
+You respond only with code blocks.

prompts/dafny_eval_comment/ask_for_fixed.txt

@@ -0,0 +1,5 @@
+This answer got Dafny verification error:
+{error}
+Please try again by taking the Dafny feedback.
+
+If an error appears in one of method ending with `_valid`, that means annotations of an existing function were altered.

prompts/dafny_eval_comment/rewrite.txt

@@ -0,0 +1,6 @@
+Given a Dafny program with function signature, preconditions, postconditions, and code, but with annotations missing.
+Please return a complete Dafny program with the strongest possible annotations (loop invariants, assert statements, etc.) filled back in.
+Use extensive comments in the code, but don't explain anything outside of it.
+Please use exactly the same function signature, preconditions, and postconditions. Do not ever modify the given lines.
+Below is the program:
+{program}

prompts/dafny_eval_comment/sys.txt

@@ -0,0 +1,4 @@
+You are an expert in Dafny.
+You will be given tasks dealing with Dafny programs including precise annotations.
+You respond only with code blocks.
+You will write a comment explaining each significant point of the program on a line before.

prompts/dafny_eval_comment_without_impls/ask_for_fixed.txt

@@ -0,0 +1,5 @@
+This answer got Dafny verification error:
+{error}
+Please try again by taking the Dafny feedback.
+
+If an error appears in one of method ending with `_valid`, that means annotations of an existing function were altered.

prompts/dafny_eval_comment_without_impls/rewrite.txt

@@ -0,0 +1,6 @@
+Given a Dafny program with function signature, preconditions and postconditions, but with some implementations and annotations missing.
+Please return a complete Dafny program with all functions implemented, and annotated using the strongest possible annotations (loop invariants, assert statements, etc.).
+Use extensive comments in the code, but don't explain anything outside of it.
+Please use exactly the same function signature, preconditions, and postconditions. Do not ever modify the given lines.
+Below is the program:
+{program}

prompts/dafny_eval_comment_without_impls/sys.txt

@@ -0,0 +1,4 @@
+You are an expert in Dafny.
+You will be given tasks dealing with Dafny programs including precise annotations.
+You respond only with code blocks.
+You will write a comment explaining each significant point of the program on a line before.