Merge branch 'master' into _update-deps/runtimeverification/k

1_k/4_imp++/lesson_2/imp.k

@@ -48,7 +48,7 @@ module IMP
   rule <k> X:Id => I ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> I ...</store>
-  rule I1 / I2 => I1 /Int I2  when I2 =/=Int 0
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
   rule I1 + I2 => I1 +Int I2
   rule - I => 0 -Int I
 // BExp

1_k/4_imp++/lesson_3/imp.k

@@ -51,7 +51,7 @@ module IMP
   rule <k> ++X => I +Int 1 ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (I => I +Int 1) ...</store>
-  rule I1 / I2 => I1 /Int I2  when I2 =/=Int 0
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
   rule I1 + I2 => I1 +Int I2
   rule - I => 0 -Int I
 // BExp

1_k/4_imp++/lesson_4/imp.k

@@ -55,7 +55,7 @@ module IMP
        <store>... N |-> (I => I +Int 1) ...</store>
   rule <k> read() => I ...</k>
        <input> ListItem(I:Int) => .List ...</input>
-  rule I1 / I2 => I1 /Int I2  when I2 =/=Int 0
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
   rule I1 + I2 => I1 +Int I2
   rule - I => 0 -Int I
   rule Str1 + Str2 => Str1 +String Str2

1_k/4_imp++/lesson_5/imp.k

@@ -54,7 +54,7 @@ module IMP
        <store>... N |-> (I => I +Int 1) ...</store>
   rule <k> read() => I ...</k>
        <input> ListItem(I:Int) => .List ...</input>
-  rule I1 / I2 => I1 /Int I2  when I2 =/=Int 0
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
   rule I1 + I2 => I1 +Int I2
   rule - I => 0 -Int I
   rule Str1 + Str2 => Str1 +String Str2

1_k/4_imp++/lesson_8/imp.md

@@ -302,7 +302,7 @@ configuration.
 ### Arithmetic constructs
 
 ```k
-  rule I1 / I2 => I1 /Int I2  when I2 =/=Int 0
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
   rule I1 + I2 => I1 +Int I2
   rule - I => 0 -Int I
 ```

2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md

@@ -241,7 +241,7 @@ right type to the allocated locations.
        <store>... .Map => L |-> array(T, L +Int 1, N)
                           (L +Int 1)...(L +Int N) |-> undefined(T) ...</store>
        <nextLoc> L:Int => L +Int 1 +Int N </nextLoc>
-    when N >=Int 0
+    requires N >=Int 0
 
   context _:Type _::Exp[HOLE::Exps];
 ```
@@ -312,8 +312,8 @@ When done with the first pass, call `main()`.
   rule Str1 + Str2 => Str1 +String Str2
   rule I1 - I2 => I1 -Int I2
   rule I1 * I2 => I1 *Int I2
-  rule I1 / I2 => I1 /Int I2 when I2 =/=K 0
-  rule I1 % I2 => I1 %Int I2 when I2 =/=K 0
+  rule I1 / I2 => I1 /Int I2 requires I2 =/=K 0
+  rule I1 % I2 => I1 %Int I2 requires I2 =/=K 0
   rule - I => 0 -Int I
   rule I1 < I2 => I1 <Int I2
   rule I1 <= I2 => I1 <=Int I2
@@ -338,7 +338,7 @@ Check array bounds, as part of the dynamic typing policy.
 
 // Same comment as for simple untyped regarding [anywhere]
   rule array(_:Type, L:Int, M:Int)[N:Int] => lookup(L +Int N)
-    when N >=Int 0 andBool N <Int M  [anywhere]
+    requires N >=Int 0 andBool N <Int M  [anywhere]
 ```
 
 ### Size of an array
@@ -372,7 +372,7 @@ checks that that type of the returned value is expected one.
          (_ => C)
        </control>
        <env> _ => Env </env>
-    when typeOf(V) ==K T   // check the type of the returned value
+    requires typeOf(V) ==K T   // check the type of the returned value
 ```
 Like the `undefined` above, `nothing` also gets
 tagged with a type now.  The empty `return` statement is
@@ -396,7 +396,7 @@ preserved:
   context (HOLE => lvalue(HOLE)) = _
 
   rule <k> loc(L) = V:Val => V ...</k> <store>... L |-> (V' => V) ...</store>
-    when typeOf(V) ==K typeOf(V')
+    requires typeOf(V) ==K typeOf(V')
 ```
 
 ### Statements
@@ -438,7 +438,7 @@ preserved:
 We only allow printing integers and strings:
 ```k
   rule <k> print(V:Val, Es => Es); ...</k> <output>... .List => ListItem(V) </output>
-    when typeOf(V) ==K int orBool typeOf(V) ==K string
+    requires typeOf(V) ==K int orBool typeOf(V) ==K string
   rule print(.Vals); => .
 ```
 
@@ -509,7 +509,7 @@ values, in which case our semantics below works fine:
    rule <k> acquire V:Val; => . ...</k>
         <holds>... .Map => V |-> 0 ...</holds>
         <busy> Busy (.Set => SetItem(V)) </busy>
-     when (notBool(V in Busy:Set))
+     requires (notBool(V in Busy:Set))
 
    rule <k> acquire V; => . ...</k>
         <holds>... V:Val |-> (N:Int => N +Int 1) ...</holds>
@@ -520,7 +520,7 @@ values, in which case our semantics below works fine:
 ```k
    rule <k> release V:Val; => . ...</k>
         <holds>... V |-> (N => N:Int -Int 1) ...</holds>
-      when N >Int 0
+      requires N >Int 0
 
    rule <k> release V; => . ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
         <busy>... SetItem(V) => .Set ...</busy>
@@ -580,8 +580,8 @@ Sequences of locations.
 ```k
   syntax Map ::= Int "..." Int "|->" K
     [function, latex({#1}\ldots{#2}\mapsto{#3})]
-  rule N...M |-> _ => .Map  when N >Int M
-  rule N...M |-> K => N |-> K (N +Int 1)...M |-> K  when N <=Int M
+  rule N...M |-> _ => .Map  requires N >Int M
+  rule N...M |-> K => N |-> K (N +Int 1)...M |-> K  requires N <=Int M
 
 // Type of a value.
   syntax Type ::= typeOf(K)  [function]

2_languages/2_kool/1_untyped/kool-untyped.md

@@ -396,7 +396,7 @@ definition.
        <store>... .Map => L |-> array(L +Int 1, N)
                           (L +Int 1) ... (L +Int N) |-> undefined ...</store>
        <nextLoc> L:Int => L +Int 1 +Int N </nextLoc>
-    when N >=Int 0
+    requires N >=Int 0
 
 
   syntax Id ::= "$1" [token] | "$2" [token]
@@ -425,8 +425,8 @@ definition.
   rule Str1 + Str2 => Str1 +String Str2
   rule I1 - I2 => I1 -Int I2
   rule I1 * I2 => I1 *Int I2
-  rule I1 / I2 => I1 /Int I2 when I2 =/=K 0
-  rule I1 % I2 => I1 %Int I2 when I2 =/=K 0
+  rule I1 / I2 => I1 /Int I2 requires I2 =/=K 0
+  rule I1 % I2 => I1 %Int I2 requires I2 =/=K 0
   rule - I => 0 -Int I
   rule I1 < I2 => I1 <Int I2
   rule I1 <= I2 => I1 <=Int I2
@@ -535,14 +535,14 @@ from SIMPLE unchanged.
   rule <k> acquire V:Val; => . ...</k>
        <holds>... .Map => V |-> 0 ...</holds>
        <busy> Busy (.Set => SetItem(V)) </busy>
-    when (notBool(V in Busy:Set))
+    requires (notBool(V in Busy:Set))
 
   rule <k> acquire V; => . ...</k>
        <holds>... V:Val |-> (N:Int => N +Int 1) ...</holds>
 
   rule <k> release V:Val; => . ...</k>
        <holds>... V |-> (N => N:Int -Int 1) ...</holds>
-    when N >Int 0
+    requires N >Int 0
 
   rule <k> release V; => . ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
        <busy>... SetItem(V) => .Set ...</busy>
@@ -584,8 +584,8 @@ from SIMPLE unchanged.
 
   syntax Map ::= Int "..." Int "|->" K
     [function, latex({#1}\ldots{#2}\mapsto{#3})]
-  rule N...M |-> _ => .Map  when N >Int M
-  rule N...M |-> K => N |-> K (N +Int 1)...M |-> K  when N <=Int M
+  rule N...M |-> _ => .Map  requires N >Int M
+  rule N...M |-> K => N |-> K (N +Int 1)...M |-> K  requires N <=Int M
 ```
 
 ## Changes to the existing untyped SIMPLE semantics
@@ -858,9 +858,9 @@ current object is not altered by `super`, so future method
 invocations see the entire object, as needed for dynamic method dispatch.
 ```k
   rule <k> X:Id => this . X ...</k> <env> Env:Map </env>
-    when notBool(X in keys(Env))
+    requires notBool(X in keys(Env))
 
-  context HOLE._::Id when (HOLE =/=K super)
+  context HOLE._::Id requires (HOLE =/=K super)
 
 // TODO: explain how Assoc matching has been replaced with two rules here.
 // Maybe also improve it a bit.
@@ -875,7 +875,7 @@ invocations see the entire object, as needed for dynamic method dispatch.
     => lookupMember(ListItem(envStackFrame(Class,Env)) EStack, X)
   rule objectClosure(Class:Id, (ListItem(envStackFrame(Class':Id,_)) => .List) _)
        . _X:Id
-    when Class =/=K Class'
+    requires Class =/=K Class'
 
 /*  rule <k> super . X => lookupMember(EStack, X) ...</k>
        <crntClass> Class </crntClass>
@@ -886,7 +886,7 @@ invocations see the entire object, as needed for dynamic method dispatch.
   rule <k> super . _X ...</k>
        <crntClass> Class </crntClass>
        <envStack> ListItem(envStackFrame(Class':Id,_)) => .List ...</envStack>
-    when Class =/=K Class'
+    requires Class =/=K Class'
 ```
 ## Method invocation
 
@@ -916,9 +916,9 @@ method call or the array access.
 
   rule <k> (X:Id => this . X)(_:Exps) ...</k>
        <env> Env </env>
-    when notBool(X in keys(Env))
+    requires notBool(X in keys(Env))
 
-  context HOLE._::Id(_) when HOLE =/=K super
+  context HOLE._::Id(_) requires HOLE =/=K super
 
   rule (objectClosure(_, EStack) . X
     => lookupMember(EStack, X:Id))(_:Exps)
@@ -934,7 +934,7 @@ method call or the array access.
   rule <k> (super . _X)(_:Exps) ...</k>
        <crntClass> Class </crntClass>
        <envStack> ListItem(envStackFrame(Class':Id,_)) => .List ...</envStack>
-    when Class =/=K Class'
+    requires Class =/=K Class'
 
   // TODO(KORE): fix getKLabel #1801
   rule (A:Exp(B:Exps))(C:Exps) => A(B) ~> #freezerFunCall(C)
@@ -968,7 +968,7 @@ argument does not evaluate to an object.
        instanceOf C => true
 
   rule objectClosure(_, (ListItem(envStackFrame(C,_)) => .List) _)
-       instanceOf C'  when C =/=K C'
+       instanceOf C'  requires C =/=K C'
 //TODO: remove the sort cast ::Id of C above, when sort inference bug fixed
 
   rule objectClosure(_, .List) instanceOf _ => false
@@ -1005,7 +1005,7 @@ evaluated, and finally the second rule initiates the lookup for the
 member's location based on the current class of the object.
 ```k
   rule <k> lvalue(X:Id => this . X) ...</k>  <env> Env </env>
-    when notBool(X in keys(Env))
+    requires notBool(X in keys(Env))
 
   context lvalue((HOLE . _)::Exp)
 
@@ -1020,7 +1020,7 @@ member's location based on the current class of the object.
                               X))
   rule lvalue(objectClosure(Class, (ListItem(envStackFrame(Class':Id,_)) => .List) _)
               . _X)
-    when Class =/=K Class'
+    requires Class =/=K Class'
 ```
 
 ## Lookup member
@@ -1043,7 +1043,7 @@ starting with the most concrete class and going up in the hierarchy.
 //    when notBool(X in keys(Env))
   rule lookupMember(ListItem(envStackFrame(_, Env)) Rest, X) =>
        lookupMember(Rest, X)
-    when notBool(X in keys(Env))
+    requires notBool(X in keys(Env))
 //TODO: beautify the above
 
 endmodule

2_languages/2_kool/2_typed/2_static/kool-typed-static.md

@@ -363,7 +363,7 @@ typed SIMPLE, so we do not discuss them much here.
 
   rule read() => int
 
-  rule print(T:Type, Ts => Ts); when T ==K int orBool T ==K string
+  rule print(T:Type, Ts => Ts); requires T ==K int orBool T ==K string
   rule print(.Types); => stmt
 
 
@@ -407,7 +407,7 @@ typed SIMPLE, so we do not discuss them much here.
 // We would like to say:
 //  context ltype(HOLE:LValue)
 // but we currently cannot type the HOLE
-  context ltype(HOLE) when isLValue(HOLE)
+  context ltype(HOLE) requires isLValue(HOLE)
 
 // OLD approach:
 //  syntax Exp ::= ltype(Exp)  [function]
@@ -459,7 +459,7 @@ at the end of this module).
 ```k
   rule <k> T:Type X:Id; => checkType(T) ~> stmt ...</k>
        <ctenvT> Rho (.Map => X |-> T) </ctenvT>
-    when notBool(X in keys(Rho))
+    requires notBool(X in keys(Rho))
 
   rule <k> T:Type X:Id; => stuck(T X;) ...</k>
        <ctenvT>... X |-> _ ...</ctenvT>
@@ -633,7 +633,7 @@ checks for cycles.
          <baseClasses> SetItem(C) Cs:Set (.Set => SetItem(C')) </baseClasses>
        ...</classData>
        <classData>... <className>C</className> <baseClass>C'</baseClass> ...</classData>
-    when notBool(C' in (SetItem(C) Cs))  [priority(25)]
+    requires notBool(C' in (SetItem(C) Cs))  [priority(25)]
 
   rule (<T>...
           <className> C </className>
@@ -713,7 +713,7 @@ wait.  Finally, the sixth rule below reports an error when the
 
   rule <k> X:Id => this . X ...</k>
        <tenv> Rho </tenv>
-    when notBool(X in keys(Rho))
+    requires notBool(X in keys(Rho))
 
 // OLD approach:
 //  rule ltype(E:Exp . X:Id) => E . X
@@ -726,7 +726,7 @@ wait.  Finally, the sixth rule below reports an error when the
        <className> C1 </className>
        <baseClass> C2:Id </baseClass>
        <ctenv> Rho </ctenv>
-    when notBool(X in keys(Rho))
+    requires notBool(X in keys(Rho))
 
   rule <k> `class`(Object) . X:Id => stuck(`class`(Object) . X) ...</k>
        <inClass> C:Id </inClass>
@@ -764,7 +764,7 @@ of the language need to insert runtime checks for downcasting to be safe.
        <output>... .List => ListItem("Classes \"" +String Id2String(C1)
                               +String "\" and \"" +String Id2String(C2)
                               +String "\" are incompatible!\n") </output>
-    when notBool(C1 in S2) andBool notBool(C2 in S1)
+    requires notBool(C1 in S2) andBool notBool(C2 in S1)
 ```
 
 ## Cleanup tasks
@@ -837,7 +837,7 @@ The subclass relation introduces a subtyping relation.
 
   rule checkSubtype((T:Type,Ts),(T':Type,Ts'))
     => checkSubtype(T,T') ~> checkSubtype(Ts,Ts')
-    when Ts =/=K .Types
+    requires Ts =/=K .Types
 
   rule checkSubtype(.Types,.Types) => .
   rule checkSubtype(.Types,void) => .
@@ -851,7 +851,7 @@ check that the types used in the program actually exists
   syntax KItem ::= checkType(Types)
 
   rule checkType(T:Type,Ts:Types) => checkType(T) ~> checkType(Ts)
-    when Ts =/=K .Types
+    requires Ts =/=K .Types
   rule checkType(.Types) => .
   rule checkType(int) => .
   rule checkType(bool) => .
@@ -883,7 +883,7 @@ is co-variant in the codomain and contra-variant in the domain).
        <className> C </className>
        <baseClass> C':Id </baseClass>
        <ctenv> Rho </ctenv>
-    when notBool(F in keys(Rho))
+    requires notBool(F in keys(Rho))
 
   rule checkMethod(_:Id,_,Object) => .
 ```

2_languages/3_fun/1_untyped/1_environment/fun-untyped.md

@@ -478,8 +478,8 @@ add more values later.
 
 ```k
   rule I1 * I2 => I1 *Int I2
-  rule I1 / I2 => I1 /Int I2 when I2 =/=K 0
-  rule I1 % I2 => I1 %Int I2 when I2 =/=K 0
+  rule I1 / I2 => I1 /Int I2 requires I2 =/=K 0
+  rule I1 % I2 => I1 %Int I2 requires I2 =/=K 0
   rule I1 + I2 => I1 +Int I2
   rule S1 ^ S2 => S1 +String S2
   rule I1 - I2 => I1 -Int I2