remove import ETHEREUM-SIMULATION from SUM-TO-N-SPEC (#451)

* remove import ETHEREUM-SIMULATION from SUM-TO-N-SPEC * tests/specs/sum-to-n: formatting, explicitely require asm.k
runtimeverification · Aug 22, 2019 · 5fbb7ca · 5fbb7ca
1 parent 3ed5f6e
commit 5fbb7ca
Showing 1 changed file with 17 additions and 98 deletions.
diff --git a/tests/specs/examples/sum-to-n-spec.k b/tests/specs/examples/sum-to-n-spec.k
@@ -1,12 +1,4 @@
-
-
-
-
-
-
-
-
-
+requires "asm.k"
 requires "edsl.k"
 requires "../lemmas.k"
 
@@ -34,50 +26,9 @@ module VERIFICATION
                     ) [macro]
 endmodule
 
-
-
-
-
-
-
-
-
-
-
 module SUM-TO-N-SPEC
-    imports ETHEREUM-SIMULATION
     imports VERIFICATION
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
     rule <k> #execute ... </k>
          <mode> NORMAL </mode>
          <schedule> DEFAULT </schedule>
@@ -88,32 +39,14 @@ module SUM-TO-N-SPEC
          <program> #asMapOpCodes(#dasmOpCodes(sumToN, DEFAULT)) </program>
          <programBytes> sumToN </programBytes>
 
+         <pc>        0  => 21                                </pc>
+         <wordStack> N : WS => 0 : N *Int (N +Int 1) /Int 2 : WS </wordStack>
+         <gas>       G  => G -Int (52 *Int N +Int 27)        </gas>
 
-
-
-
-
-
-
-
-
-     <pc>        0  => 21                                </pc>
-     <wordStack> N : WS => 0 : N *Int (N +Int 1) /Int 2 : WS </wordStack>
-     <gas>       G  => G -Int (52 *Int N +Int 27)        </gas>
-
-  requires N >=Int 0
-   andBool N <=Int 340282366920938463463374607431768211455
-   andBool #sizeWordStack(WS) <Int 1021
-   andBool G >=Int 52 *Int N +Int 27
-
-
-
-
-
-
-
-
-
+      requires N >=Int 0
+       andBool N <=Int 340282366920938463463374607431768211455
+       andBool #sizeWordStack(WS) <Int 1021
+       andBool G >=Int 52 *Int N +Int 27
 
     rule <k> #execute ... </k>
          <mode> NORMAL </mode>
@@ -125,30 +58,16 @@ module SUM-TO-N-SPEC
          <program> #asMapOpCodes(#dasmOpCodes(sumToN, DEFAULT)) </program>
          <programBytes> sumToN </programBytes>
 
+         <pc>  3 => 21                         </pc>
+         <gas> G => G -Int (52 *Int I +Int 21) </gas>
 
+         <wordStack> I : S                               : WS
+                  => 0 : S +Int I *Int (I +Int 1) /Int 2 : WS </wordStack>
 
-
-
-
-
-
-
-
-
-
-
-     <pc>  3 => 21                         </pc>
-     <gas> G => G -Int (52 *Int I +Int 21) </gas>
-
-     <wordStack> I : S                               : WS
-              => 0 : S +Int I *Int (I +Int 1) /Int 2 : WS </wordStack>
-
-  requires I >=Int 0
-   andBool S >=Int 0
-   andBool S +Int I *Int (I +Int 1) /Int 2 <Int pow256
-   andBool #sizeWordStack(WS) <Int 1021
-   andBool G >=Int 52 *Int I +Int 21
+      requires I >=Int 0
+       andBool S >=Int 0
+       andBool S +Int I *Int (I +Int 1) /Int 2 <Int pow256
+       andBool #sizeWordStack(WS) <Int 1021
+       andBool G >=Int 52 *Int I +Int 21
 
 endmodule
-
-