Merge pull request #1770 from herd/aslspec-fix

[aslspec] fixed tick_loop_limit to match implementation

Author: Roman-Manevich

asllib/doc/Statements.tex

@@ -1540,6 +1540,11 @@ \subsection{Semantics}
 starts at $\nvint(4)$ and decrements towards $\nvint(0)$,
 stopping at $\nvint(1)$ on the last iteration of the loop.
 
+\ExampleDef{Negative Loop Limit Values}
+In \listingref{semantics-swhile-negative-limit}, the loop limit value starts at $\nvint(-1)$
+so the loop limit is immediately reached, resulting in a \dynamicerrorterm{} without executing the loop body at all.
+(The same would happen if the loop limit value started at $\nvint(0)$.)
+\ASLListing{A \texttt{while} statement with a negative loop limit}{semantics-swhile-negative-limit}{\semanticstests/SemanticsRule.SWhile.negative_limit.asl}
 
 \RenderProseAndFormally{tick_loop_limit}
 

asllib/doc/asl.spec

@@ -10147,14 +10147,17 @@ semantics relation tick_loop_limit(v_opt: option(N)) -> (v_opt': option(N)) | TD
   }
 
   case some_ok {
-    v_opt =: some(v);
-    v > zero;
+    v_opt =: some(limit);
+    new_limit := limit - one;
+    new_limit >= zero;
     --
-    some(v - one);
+    some(new_limit);
   }
 
   case some_error {
-    v_opt =: some(zero);
+    v_opt =: some(limit);
+    new_limit := limit - one;
+    new_limit < zero;
     --
     DynamicError(DE_LE);
   }

asllib/tests/ASLSemanticsReference.t/SemanticsRule.SWhile.negative_limit.asl

@@ -0,0 +1,8 @@
+func main () => integer
+begin
+  // A negative loop limit prevents loops from executing.
+  while TRUE looplimit -1 do
+    println "This should not be printed";
+  end;
+  return 0;
+end;

asllib/tests/ASLSemanticsReference.t/run.t

@@ -72,6 +72,14 @@ ASL Semantics Tests:
      end;
   ASL Dynamic error: loop limit reached.
   [1]
+  $ aslref SemanticsRule.SWhile.negative_limit.asl
+  File SemanticsRule.SWhile.negative_limit.asl, line 4, character 2 to line 6,
+    character 6:
+    while TRUE looplimit -1 do
+      println "This should not be printed";
+    end;
+  ASL Dynamic error: loop limit reached.
+  [1]
   $ aslref SemanticsRule.SRepeat.asl
   File SemanticsRule.SRepeat.asl, line 24, character 4 to line 31, character 17:
       repeat