in case

tests/test_nagini.py

@@ -12,8 +12,10 @@ def test_nagini_generate():
         def main(value: int) -> int:
             Requires(value >= 10)
             Ensures(Result() >= 20)
+            # impl-start
             Assert(value * 2 >= 20) # assert-line
-            return value * 2"""
+            return value * 2
+            # impl-end"""
     )
     assert nagini_lang.generate_validators(code) == dedent(
         """\
@@ -136,3 +138,109 @@ def is_prime(k : int) -> bool:
                 d_2_i_ = (d_2_i_) + (1)
             return result"""
     )
+
+
+def test_nagini_generate1():
+    nagini_lang = LanguageDatabase().get("nagini")
+
+    code = dedent(
+        """\
+        from typing import cast, List, Dict, Set, Optional, Union
+        from nagini_contracts.contracts import *
+        
+        @Pure
+        def lower(c : int) -> bool :
+            # impl-start
+            return ((0) <= (c)) and ((c) <= (25))
+            # impl-end
+        
+        @Pure
+        def upper(c : int) -> bool :
+            # impl-start
+            return ((26) <= (c)) and ((c) <= (51))
+            # impl-end
+        
+        @Pure
+        def alpha(c : int) -> bool :
+            # impl-start
+            return (lower(c)) or (upper(c))
+            # impl-end
+        
+        @Pure
+        def flip__char(c : int) -> int :
+            # pre-conditions-start
+            Ensures(lower(c) == upper(Result()))
+            Ensures(upper(c) == lower(Result()))
+            # pre-conditions-end
+        
+            # impl-start
+            if lower(c):
+                return ((c) - (0)) + (26)
+            elif upper(c):
+                return ((c) + (0)) - (26)
+            elif True:
+                return c
+            # impl-end
+        
+        def flip__case(s : List[int]) -> List[int] :
+            # pre-conditions-start
+            Requires(Acc(list_pred(s)))
+            # pre-conditions-end
+            # post-conditions-start
+            Ensures(Acc(list_pred(s)))
+            Ensures(Acc(list_pred(Result())))
+            Ensures((len(Result())) == (len(s)))
+            Ensures(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (len(s))), lower((s)[d_0_i_]) == upper((Result())[d_0_i_])))))
+            Ensures(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (len(s))), upper((s)[d_0_i_]) == lower((Result())[d_0_i_])))))
+            # post-conditions-end
+        
+            # impl-start
+            res = list([int(0)] * len(s)) # type : List[int]
+            i = int(0) # type : int
+            while i < len(s):
+                # invariants-start
+                Invariant(Acc(list_pred(s)))
+                Invariant(Acc(list_pred(res)))
+                Invariant(((0) <= (i)) and ((i) <= (len(s))))
+                Invariant((len(res)) == (len(s)))
+                Invariant(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (i)), lower((s)[d_0_i_]) == upper((res)[d_0_i_])))))
+                Invariant(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (i)), upper((s)[d_0_i_]) == lower((res)[d_0_i_])))))
+                # invariants-end
+                res[i] = flip__char(s[i])
+                i = i + 1
+            return res
+            # impl-end
+"""
+    )
+    assert nagini_lang.generate_validators(code) == dedent(
+        """\
+        def lower_valid(c : int) -> bool :
+            ret = lower(c)
+            return ret
+        def upper_valid(c : int) -> bool :
+            ret = upper(c)
+            return ret
+        def alpha_valid(c : int) -> bool :
+            ret = alpha(c)
+            return ret
+        def flip__char_valid(c : int) -> int :
+            # pre-conditions-start
+            Ensures(lower(c) == upper(Result()))
+            Ensures(upper(c) == lower(Result()))
+            # pre-conditions-end
+            ret = flip__char(c)
+            return ret
+        def flip__case_valid(s : List[int]) -> List[int] :
+            # pre-conditions-start
+            Requires(Acc(list_pred(s)))
+            # pre-conditions-end
+            # post-conditions-start
+            Ensures(Acc(list_pred(s)))
+            Ensures(Acc(list_pred(Result())))
+            Ensures((len(Result())) == (len(s)))
+            Ensures(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (len(s))), lower((s)[d_0_i_]) == upper((Result())[d_0_i_])))))
+            Ensures(Forall(int, lambda d_0_i_: (Implies(((0) <= (d_0_i_)) and ((d_0_i_) < (len(s))), upper((s)[d_0_i_]) == lower((Result())[d_0_i_])))))
+            # post-conditions-end
+            ret = flip__case(s)
+            return ret"""
+    )

verified_cogen/experiments/incremental_run.py

@@ -12,7 +12,14 @@
 from verified_cogen.tools.modes import Mode
 from verified_cogen.tools.verifier import Verifier
 
+import sys
+
 logger = logging.getLogger(__name__)
+handler = logging.StreamHandler(sys.stdout)
+
+formatter = logging.Formatter('%(asctime)s - %(levelname)s - %(message)s')
+handler.setFormatter(formatter)
+logger.addHandler(handler)
 
 
 def main():

verified_cogen/runners/languages/nagini.py

@@ -16,7 +16,8 @@ class NaginiLanguage(GenericLanguage):
     def __init__(self):
         super().__init__(
             re.compile(
-                r"def\s+(\w+)\s*\((.*?)\)\s*->\s*(.*?):((?:\r\n|\r|\n) *(?:Requires|Ensures)\(.*\)(?:\r\n|\r|\n))*",
+            #    r"def\s+(\w+)\s*\((.*?)\)\s*->\s*(.*?):((?:\r\n|\r|\n) *(?:Requires|Ensures)\(.*\)(?:\r\n|\r|\n))*",
+                r"def\s+(\w+)\s*\((.*?)\)\s*->\s*(.*?):(.*?(\r\n|\r|\n))\s+# impl-start",
                 re.DOTALL,
             ),
             NAGINI_VALIDATOR_TEMPLATE,

verified_cogen/tools/verifier.py

@@ -2,6 +2,7 @@
 import subprocess
 from pathlib import Path
 from typing import Optional
+import os
 
 log = logging.getLogger(__name__)
 
@@ -23,6 +24,7 @@ def verify(self, file_path: Path) -> Optional[tuple[bool, str, str]]:
                 timeout=self.timeout,
             )
         except subprocess.TimeoutExpired:
+            os.system("killall z3")
             return None
         return (
             res.returncode == 0,