Use keyword claim in integration tests

test/all-path/00-basic/00-no-rules/distinct-spec.k

@@ -8,6 +8,6 @@ module DISTINCT-SPEC
   imports PATH
 
   // should not be provable, as there is no axiom
-  rule <k> a => b </k> [all-path]
+  claim <k> a => b </k> [all-path]
 
 endmodule

test/all-path/00-basic/00-no-rules/identity-spec.k

@@ -7,6 +7,6 @@ module IDENTITY-SPEC
   imports VERIFICATION
   imports PATH
 
-  rule <k> a => a </k> [all-path]
+  claim <k> a => a </k> [all-path]
 
 endmodule

test/all-path/00-basic/01-one-rule/all-path-b-or-c-spec.k

@@ -7,6 +7,6 @@ module ALL-PATH-B-OR-C-SPEC
   import PATH
 
   // This should be provable as transiting to b suffices
-  rule <k> a => b #Or c </k> [all-path]
+  claim <k> a => b #Or c </k> [all-path]
 
 endmodule

test/all-path/00-basic/01-one-rule/all-path-b-spec.k

@@ -7,6 +7,6 @@ module ALL-PATH-B-SPEC
   imports PATH
 
   // This should be provable as there is only one axiom.
-  rule <k> a => b </k> [all-path]
+  claim <k> a => b </k> [all-path]
 
 endmodule

test/all-path/00-basic/01-one-rule/all-path-c-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-C-SPEC
   imports PATH
 
   // This should not be provable as the only axiom is a => b.
-  rule <k> a => c </k> [all-path]
+  claim <k> a => c </k> [all-path]
 
 endmodule

test/all-path/00-basic/02-cyclic-rule/all-path-b-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-B-SPEC
   imports PATH
 
   // Everything is provable if I can reach a cycling rule
-  rule <k> a => b </k> [all-path]
+  claim <k> a => b </k> [all-path]
 
 endmodule

test/all-path/00-basic/02-cyclic-rule/all-path-c-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-C-SPEC
   imports PATH
 
   // Everything is provable if I can reach a cycling rule
-  rule <k> a => c </k> [all-path]
+  claim <k> a => c </k> [all-path]
 
 endmodule

test/all-path/00-basic/03-concurrent-rules/all-path-b-or-c-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-B-OR-C-SPEC
   imports PATH
 
 // This should be provable as both one-path and all-path.
-  rule <k> a => b #Or c </k> [all-path]
+  claim <k> a => b #Or c </k> [all-path]
 
 endmodule

test/all-path/00-basic/03-concurrent-rules/all-path-b-spec.k

@@ -9,6 +9,6 @@ module ALL-PATH-B-SPEC
 
   // This should be provable as an one-path claim, but should not be provable as an 
   //all-path claim.
-  rule <k> a => c </k> [all-path]
+  claim <k> a => c </k> [all-path]
 
 endmodule

test/all-path/00-basic/03-concurrent-rules/one-path-b-spec.k

@@ -9,6 +9,6 @@ module ONE-PATH-B-SPEC
 
   // This should be provable as an one-path claim, but should not be provable as an 
   //all-path claim.
-  rule <k> a => c </k> [one-path]
+  claim <k> a => c </k> [one-path]
 
 endmodule

test/all-path/00-basic/04-different-length/all-path-f-spec.k

@@ -8,5 +8,5 @@ module ALL-PATH-F-SPEC
   imports PATH
 
   // This should be provable as both one-path and all-path.
-  rule <k> a => f </k> [all-path]
+  claim <k> a => f </k> [all-path]
 endmodule

test/all-path/02-constructors/00-case-analysis/all-path-partial-spec.k

@@ -9,6 +9,6 @@ module ALL-PATH-PARTIAL-SPEC
 
   // This should not be provable both one-path and all-path.
   // because it does not hold for X = c
-  rule <k> partial(X:S) => end </k> [all-path]
+  claim <k> partial(X:S) => end </k> [all-path]
 
 endmodule

test/all-path/02-constructors/00-case-analysis/all-path-total-spec.k

@@ -9,6 +9,6 @@ module ALL-PATH-TOTAL-SPEC
 
   // This should be provable as both one-path and all-path.
   // Note that this uses that S is only formed of a | b | c
-  rule <k> total(X:S) => end </k> [all-path]
+  claim <k> total(X:S) => end </k> [all-path]
 
 endmodule

test/all-path/03-unification/set-select/all-path-b-or-c-spec.k

@@ -7,7 +7,7 @@ module ALL-PATH-B-OR-C-SPEC
   imports VERIFICATION
   imports PATH
 
-  rule <k> select => b #Or c </k>
+  claim <k> select => b #Or c </k>
        <state> SetItem(b) SetItem(c) </state>
     [all-path]
 

test/all-path/03-unification/set-select/all-path-b-spec.k

@@ -9,7 +9,7 @@ module ALL-PATH-B-SPEC
 
   // This should be provable as an one-path claim, but should not be provable as an 
   //all-path claim.
-  rule <k> select => b </k>
+  claim <k> select => b </k>
        <state> SetItem(b) SetItem(c) </state> [all-path]
 
 endmodule

test/all-path/03-unification/set-select/all-path-select-a-b-c-spec.k

@@ -9,7 +9,7 @@ module ALL-PATH-SELECT-A-B-C-SPEC
 
   // This should be provable as an one-path claim, but should not be provable as an
   //all-path claim.
-  rule <k> select => b #Or c </k>
+  claim <k> select => b #Or c </k>
        <state> SetItem(a) SetItem(b) SetItem(c) </state> [all-path]
 
 endmodule

test/all-path/03-unification/set-select/one-path-b-or-c-spec.k

@@ -7,7 +7,7 @@ module ONE-PATH-B-OR-C-SPEC
   imports VERIFICATION
   imports PATH
 
-  rule <k> select => b #Or c </k>
+  claim <k> select => b #Or c </k>
        <state> SetItem(b) SetItem(c) </state>
     [one-path]
 

test/all-path/03-unification/set-select/one-path-b-spec.k

@@ -9,7 +9,7 @@ module ONE-PATH-B-SPEC
 
   // This should be provable as an one-path claim, but should not be provable as an 
   //all-path claim.
-  rule <k> select => b </k>
+  claim <k> select => b </k>
        <state> SetItem(b) SetItem(c) </state>
     [one-path]
 

test/all-path/03-unification/set-select/one-path-c-spec.k

@@ -9,7 +9,7 @@ module ONE-PATH-C-SPEC
 
   // This should be provable as an one-path claim, but should not be provable as an 
   //all-path claim.
-  rule <k> select => b </k>
+  claim <k> select => b </k>
        <state> SetItem(b) SetItem(c) </state>
     [one-path]
 

test/all-path/limitations/interfering-specs/all-path-a-c-b-d-spec.k

@@ -13,7 +13,7 @@ module ALL-PATH-A-C-B-D-SPEC
   imports VERIFICATION
   imports PATH
 
-  rule <k> a => c </k> [all-path]
-  rule <k> b => d </k> [all-path]
+  claim <k> a => c </k> [all-path]
+  claim <k> b => d </k> [all-path]
 
 endmodule

test/all-path/limitations/interfering-specs/all-path-a-c-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-A-C-SPEC
   imports PATH
 
   // This should be provable
-  rule <k> a => c </k> [all-path]
+  claim <k> a => c </k> [all-path]
 
 endmodule

test/all-path/limitations/interfering-specs/all-path-b-d-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-B-D-SPEC
   imports PATH
 
   // This should be provable
-  rule <k> b => d </k> [all-path]
+  claim <k> b => d </k> [all-path]
 
 endmodule

test/assume/test-spec.k

@@ -7,6 +7,6 @@ endmodule
 module TEST-SPEC
     imports VERIFICATION
 
-    rule <k> #assume false => . </k>
+    claim <k> #assume false => . </k>
 
 endmodule

test/bmc/fail-1-bmc-spec.k

@@ -11,6 +11,6 @@ module FAIL-1-BMC-SPEC
   imports VERIFICATION
   imports BMC
 
-  rule (<T> <k> #execute </k> <state> "x" |-> 6 </state> </T>) #Implies (#AG (#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X <Int 10 #Equals true})))  [kore]
+  claim (<T> <k> #execute </k> <state> "x" |-> 6 </state> </T>) #Implies (#AG (#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X <Int 10 #Equals true})))  [kore]
 
 endmodule

test/bmc/fail-2-non-positive-bmc-spec.k

@@ -11,6 +11,6 @@ module FAIL-2-NON-POSITIVE-BMC-SPEC
   imports VERIFICATION
   imports BMC
 
-  rule (<T> <k> #execute </k> <state> "x" |-> X </state> </T> #And {X >Int 0 #Equals false}) #Implies (#AG(#Forall Y . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> Y </state> </T>) #Implies {X ==Int Y #Equals true})))  [kore]
+  claim (<T> <k> #execute </k> <state> "x" |-> X </state> </T> #And {X >Int 0 #Equals false}) #Implies (#AG(#Forall Y . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> Y </state> </T>) #Implies {X ==Int Y #Equals true})))  [kore]
 
 endmodule

test/bmc/fail-2-positive-bmc-spec.k

@@ -11,6 +11,6 @@ module FAIL-2-POSITIVE-BMC-SPEC
   imports VERIFICATION
   imports BMC
 
-  rule (<T> <k> #execute </k> <state> "x" |-> X </state> </T> #And {X >Int 0 #Equals true}) #Implies (#AG(#Forall Y . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> Y </state> </T>) #Implies {X ==Int Y #Equals true})))  [kore]
+  claim (<T> <k> #execute </k> <state> "x" |-> X </state> </T> #And {X >Int 0 #Equals true}) #Implies (#AG(#Forall Y . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> Y </state> </T>) #Implies {X ==Int Y #Equals true})))  [kore]
 
 endmodule

test/bmc/fail-3-bmc-spec.k

@@ -11,6 +11,6 @@ module FAIL-3-BMC-SPEC
   imports VERIFICATION
   imports BMC
 
-  rule (<T> <k> #execute </k> <state> "x" |-> X </state> </T> #And {0 <Int X #Equals true}) #Implies (#AG(#Forall Y . #Forall _ .((<T> <k> _ </k> <state> "x" |-> Y </state> </T>) #Implies {0 <Int Y #Equals true})))  [kore]
+  claim (<T> <k> #execute </k> <state> "x" |-> X </state> </T> #And {0 <Int X #Equals true}) #Implies (#AG(#Forall Y . #Forall _ .((<T> <k> _ </k> <state> "x" |-> Y </state> </T>) #Implies {0 <Int Y #Equals true})))  [kore]
 
 endmodule

test/bmc/fail-4-bmc-spec.k

@@ -11,6 +11,6 @@ module FAIL-4-BMC-SPEC
   imports VERIFICATION
   imports BMC
 
-  rule (<T> <k> #execute </k> <state> "x" |-> X </state> </T> #And {(5 <Int X andBool X <Int 8) #Equals true}) #Implies (#AG(#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X <Int 8 #Equals true})))  [kore]
+  claim (<T> <k> #execute </k> <state> "x" |-> X </state> </T> #And {(5 <Int X andBool X <Int 8) #Equals true}) #Implies (#AG(#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X <Int 8 #Equals true})))  [kore]
 
 endmodule

test/bmc/pass-1-bmc-spec.k

@@ -11,6 +11,6 @@ module PASS-1-BMC-SPEC
   imports VERIFICATION
   imports BMC
 
-  rule (<T> <k> #execute </k> <state> "x" |-> -3 </state> </T>) #Implies (#AG(#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X <=Int 0 #Equals true})))  [kore]
+  claim (<T> <k> #execute </k> <state> "x" |-> -3 </state> </T>) #Implies (#AG(#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X <=Int 0 #Equals true})))  [kore]
 
 endmodule

test/bmc/pass-2-bmc-spec.k

@@ -11,6 +11,6 @@ module PASS-2-BMC-SPEC
   imports VERIFICATION
   imports BMC
 
-  rule (<T> <k> #execute </k> <state> "x" |-> 0 </state> </T>) #Implies (#AG(#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X ==Int 0 #Equals true})))  [kore]
+  claim (<T> <k> #execute </k> <state> "x" |-> 0 </state> </T>) #Implies (#AG(#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X ==Int 0 #Equals true})))  [kore]
 
 endmodule

test/bmc/pass-3-bmc-spec.k

@@ -11,6 +11,6 @@ module PASS-3-BMC-SPEC
   imports VERIFICATION
   imports BMC
 
-  rule (<T> <k> #execute </k> <state> "x" |-> 2 </state> </T>) #Implies (#AG(#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X ==Int 2 #Equals true})))  [kore]
+  claim (<T> <k> #execute </k> <state> "x" |-> 2 </state> </T>) #Implies (#AG(#Forall X . #Forall _ .((<T> <k> #execute </k> <state> "x" |-> X </state> </T>) #Implies {X ==Int 2 #Equals true})))  [kore]
 
 endmodule

test/functions/length-cons-spec.k

@@ -10,12 +10,12 @@ module LENGTH-CONS-SPEC
   imports VERIFICATION
 
   // test claim
-  rule
+  claim
     <k> begin => end </k>
     <n> X:KItem : XS:ConsList </n>
 
   // applies only if initial condition applied
-  rule
+  claim
     <k> next _ => end </k>
     <n> X:KItem : XS:ConsList </n>
     requires length(X : XS) >Int length(XS)

test/functions/length-spec.k

@@ -10,13 +10,13 @@ module LENGTH-SPEC
   imports VERIFICATION
 
   // test claim
-  rule
+  claim
     <k> begin => end </k>
     <n> LIST:ConsList </n>
     requires length(LIST) >Int 1
 
   // applies only if initial condition applied
-  rule
+  claim
     <k> next _ => end </k>
     <n> LIST:ConsList </n>
     requires length(LIST) >Int 1

test/functions/positive-requires-spec.k

@@ -10,13 +10,13 @@ module POSITIVE-REQUIRES-SPEC
   imports VERIFICATION
 
   // test claim
-  rule
+  claim
     <k> begin => end </k>
     <n> N </n>
     requires N >Int 0
 
   // applies only if `positive` is defined
-  rule
+  claim
     <k> next _ => end </k>
     <n> N </n>
     requires positive(N)

test/functions/positive-spec.k

@@ -10,13 +10,13 @@ module POSITIVE-SPEC
   imports VERIFICATION
 
   // test claim
-  rule
+  claim
     <k> begin => end </k>
     <n> N </n>
     requires N >Int 0
 
   // applies only if `positive` is defined
-  rule
+  claim
     <k> next positive(N) => end </k>
     <n> N </n>
     [trusted]

test/imp/add-spec.k

@@ -12,7 +12,7 @@ module ADD-SPEC
   imports VERIFICATION
   imports IMP
 
-  rule
+  claim
     <k>
 sum = 1 + 1;
 => .K

test/imp/double-sum-spec.k

@@ -14,7 +14,7 @@ module DOUBLE-SUM-SPEC
   imports VERIFICATION
 
 
-rule
+claim
     <k>
       while (!(n <= 0)) {
         sum = sum + n + n;
@@ -29,7 +29,7 @@ rule
   </state>
 requires N >=Int 0
 
-rule
+claim
     <k>
       int n, sum;
       n = N:Int;

test/imp/max-spec.k

@@ -14,7 +14,7 @@ module MAX-SPEC
   imports VERIFICATION
   imports IMP
 
-  rule
+  claim
     <k>
       if (a <= b) {
           max = b;

test/imp/sum-div-spec.k

@@ -15,7 +15,7 @@ module SUM-DIV-SPEC
   imports VERIFICATION
 
 
-  rule
+  claim
     <k>
       while (!(n <= 0)) {
           sum = sum + n;
@@ -30,7 +30,7 @@ module SUM-DIV-SPEC
     </state>
   requires N >=Int 0
 
-  rule
+  claim
     <k>
       int n, sum;
       n = N:Int;

test/imp/sum-save-proofs-spec.k

@@ -15,7 +15,7 @@ module SUM-SAVE-PROOFS-SPEC
   imports VERIFICATION
 
 
-rule
+claim
     <k>
       while (!(n <= 0)) {
         sum = sum + n + n;
@@ -30,7 +30,7 @@ rule
   </state>
 requires N >=Int 0
 
-rule
+claim
     <k>
       int n, sum;
       n = N:Int;