Smart search

prompts/humaneval-nagini-few-shot-comments/add.txt

@@ -0,0 +1,6 @@
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+The program:
+{program}
+–
+The invariants:
+{checks}

prompts/humaneval-nagini-few-shot-comments/ask_for_fixed.txt

@@ -0,0 +1,6 @@
+The following errors occurred during verification:
+{error}
+
+Please fix the error by adding, removing or modifying the invariants and asserts and return the fixed program.
+Use extensive comments in the code, but don't explain anything outside of it.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.

prompts/humaneval-nagini-few-shot-comments/ask_for_fixed_had_errors.txt

@@ -0,0 +1,6 @@
+There are still some errors:
+{error}
+
+Could you please fix them?
+Use extensive comments in the code, but don't explain anything outside of it.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.

prompts/humaneval-nagini-few-shot-comments/produce.txt

@@ -0,0 +1,80 @@
+Given the following Python program, output Nagini invariants that should go into the `while` loop.
+Ensure that the invariants are as comprehensive as they can be.
+Even if you think some invariant is not totally necessary, better add it than not.
+Don't add any additional text comments, your response must contain only program with invariants.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+
+You remember the following aspects of Nagini syntax:
+
+1. Nagini DOES NOT SUPPORT some Python features as list comprehensions (k + 1 for k in range(5)), as double inequalities (a <= b <= c).
+Instead of double inequalities it's customary to use two separate inequalities (a <= b and b <= c).
+
+2. In Nagini method preconditions (Requires) and postconditions (Ensures) placed right after method signature, like here:
+"
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+    Ensures(Acc(list_pred(a)))
+    ...
+"
+
+3. Invariant are placed right after `while` statement and before the code of `while` body:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        s = s + numbers[i]
+"
+Invariants CANNOT be placed in any other position.
+You remember that each invariant (and each expression) should contain equal number of opening and closing brackets, so that it is valid.
+You should sustain balanced parentheses.
+
+4. Nagini requires special annotations for working with lists `Acc(list_pred(..))`. You can use these constructs only inside `Invariant`,
+anywhere else you should not use `Acc()` or `list_pred()`:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+"
+
+5. Nagini contains `Forall` and `Exists` constructs that can be used in invariants. First argument of Forall/Exists is typically a type (i.e `int`),
+second argument is a lambda. `Forall(type, lambda x : a)` denotes that assertion `a` is true for every element `x` of type `type`.
+
+6. In Nagini `Implies(e1, a2)` plays role of implication. `Implies(e1, a2)` denotes that assertion a2 holds if boolean expression e1 is true.
+You can use it inside invariants and asserts.
+
+Here are some examples of verified Python cycles with Nagini invariants:
+```
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(Acc(list_pred(result)))
+        Invariant(0 <= i and i <= len(numbers))
+        Invariant(len(result) == i)
+        Invariant(Forall(range(i), lambda i1: numbers[i1] <= result[i1]))
+        Invariant(Old(running_max) is None or ((Old(running_max) is not None) and (getVal(Old(running_max)) <= getVal(running_max))))
+        Invariant(Implies(len(result) > 0, running_max is not None))
+        Invariant(Implies(len(result) > 0, result[-1] == getVal(running_max)))
+        Invariant(Forall(range(i - 1), lambda i1: result[i1] <= result[i1 + 1]))
+
+        n = numbers[i]
+        if running_max is None or running_max < n:
+            running_max = n
+
+        result.append(running_max)
+        i += 1
+```
+
+```
+    while (d_0_i_) < (len((a))):
+        Invariant(Acc(list_pred(c)))
+        Invariant(Acc(list_pred(a)))
+        Invariant(len(c) == len(a) + 1)
+        Invariant(((0) <= (d_0_i_)) and ((d_0_i_) <= (len((a)))))
+        Invariant(Forall(int, lambda d_1_ii_:
+            Implies(((0) <= (d_1_ii_)) and ((d_1_ii_) < (d_0_i_)), ((c)[d_1_ii_]) == ((a)[d_1_ii_]))))
+        (c)[(d_0_i_)] = (a)[d_0_i_]
+        d_0_i_ = (d_0_i_) + (1)
+```
+
+The program:
+{program}
+

prompts/humaneval-nagini-few-shot-comments/rewrite.txt

@@ -0,0 +1,79 @@
+Rewrite the following Python program, adding correct Nagini invariants into `while` loops.
+Do not change the code, only add the invariants.
+Ensure that the invariants are as comprehensive as they can be.
+Even if you think some invariant is not totally necessary, better add it than not.
+Use extensive comments in the code, but don't explain anything outside of it.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+
+You remember the following aspects of Nagini syntax:
+
+1. Nagini DOES NOT SUPPORT some Python features as list comprehensions (k + 1 for k in range(5)), as double inequalities (a <= b <= c).
+Instead of double inequalities it's customary to use two separate inequalities (a <= b and b <= c).
+
+2. In Nagini method preconditions (Requires) and postconditions (Ensures) placed right after method signature, like here:
+"
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+    Ensures(Acc(list_pred(a)))
+    ...
+"
+
+3. Invariant are placed right after `while` statement and before the code of `while` body:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        s = s + numbers[i]
+"
+Invariants CANNOT be placed in any other position.
+You remember that each invariant (and each expression) should contain equal number of opening and closing brackets, so that it is valid.
+You should sustain balanced parentheses.
+
+4. Nagini requires special annotations for working with lists `Acc(list_pred(..))`. You can use these constructs only inside `Invariant`,
+anywhere else you should not use `Acc()` or `list_pred()`:
+"
+    while i < len(numbers):
+        Invariant(Acc(list_pred(numbers)))
+"
+
+5. Nagini contains `Forall` and `Exists` constructs that can be used in invariants. First argument of Forall/Exists is typically a type (i.e `int`),
+second argument is a lambda. `Forall(type, lambda x : a)` denotes that assertion `a` is true for every element `x` of type `type`.
+
+6. In Nagini `Implies(e1, a2)` plays role of implication. `Implies(e1, a2)` denotes that assertion a2 holds if boolean expression e1 is true.
+You can use it inside invariants and asserts.
+
+You might need to work with accumulating functions, such as sum, so here's an example of how to do that:
+```
+from typing import cast, List, Dict, Set, Optional, Union
+from nagini_contracts.contracts import *
+
+@Pure
+def Sum(a : List[int], s : int, t : int) -> int :
+    Requires(Acc(list_pred(a)))
+    Requires(((0) <= (s)) and ((s) <= (t)) and ((t) <= (len(a))))
+
+    if s == t:
+        return 0
+    else:
+        return (a)[t - 1] + (Sum(a, s, t - 1))
+
+def sum_loop(numbers: List[int]) -> int:
+    Requires(Acc(list_pred(numbers)))
+    Ensures(Acc(list_pred(numbers)))
+    Ensures(Result() == Sum(numbers, 0, len(numbers)))
+    s = int(0)
+    i = int(0)
+    while (i) < (len(numbers)):
+        Invariant(Acc(list_pred(numbers)))
+        Invariant(0 <= i and i <= len(numbers))
+        Invariant(Forall(int, lambda d_1_p_:
+            (Implies(0 <= d_1_p_ and d_1_p_ < len(numbers), Sum(numbers, 0, d_1_p_ + 1) == Sum(numbers, 0, d_1_p_) + numbers[d_1_p_]), [[Sum(numbers, 0, d_1_p_ + 1)]])))
+        Invariant(s == Sum(numbers, 0, i))
+        Assert(Sum(numbers, 0, i + 1) == Sum(numbers, 0, i) + numbers[i])
+        s = s + (numbers)[i]
+        i = i + 1
+    return s
+```
+The program:
+{program}

prompts/humaneval-nagini-few-shot-comments/sys.txt

@@ -0,0 +1,4 @@
+You are an expert in a Python verification framework Nagini.
+You will be given tasks dealing with Python programs including precise docstrings and specifications.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.
+Take into account that arrays inside the invariants are indexed by type `int`.

prompts/humaneval-nagini-few-shot-comments/timeout.txt

@@ -0,0 +1,3 @@
+The verifier timed out during the verification.
+This usually means that the provided invariants were too broad or were difficult to check.
+Could you please try to improve the invariants and try again?

prompts/humaneval-nagini-without-impls-cot-instruct/ask_for_fixed.txt

@@ -0,0 +1,7 @@
+The following errors occurred during verification:
+{error}
+
+Please fix the error by adding, removing or modifying the implementation, invariants or assertions and return the fixed program.
+You should not modify any helper functions (annotated with @Pure), remember they are here to help you with verification.
+Don't add any additional text comments, your response must contain only program with invariants.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.

prompts/humaneval-nagini-without-impls-cot-instruct/ask_for_fixed_had_errors.txt

@@ -0,0 +1,7 @@
+There are still some errors:
+{error}
+
+Please fix the error by adding, removing or modifying the implementation, invariants or assertions and return the fixed program.
+You should not modify any helper functions (annotated with @Pure), remember they are here to help you with verification.
+Don't add any additional text comments, your response must contain only program with invariants.
+Do not provide ANY explanations. Don't include markdown backticks. Respond only in Python code, nothing else.

prompts/humaneval-nagini-without-impls-cot-instruct/helpers.txt

@@ -0,0 +1,2 @@
+Generally, you should use helper functions (marked with @Pure annotation) only in invariants, asserts and conditions (in `if` or `while` conditions), not in the plain code.
+But, the following helper functions you can use anywhere: {helpers}.

prompts/humaneval-nagini-without-impls-cot-instruct/invalid_helpers.txt

@@ -0,0 +1,9 @@
+We detected an improper usage of helper functions. Here is the list of helper functions used in a wrong way:
+{invalid_helpers}
+You should use helper functions only in invariants, asserts and conditions (in `if` or `while` conditions), not in the plain code.
+The following helper functions you can use anywhere: {helpers}.
+We replaced all improper usages with `invalid_call()` and got the following program:
+{program}
+You should rewrite this program without changing pre/postconditions and helper functions (denoted with @Pure).
+After rewriting your code should verify.
+Your code should not contain any `invalid_call()` invocations.