Specification int-div

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   int-mult
with
   comment: Integer division and remainder. The remainder can be negative, hence it is not
         the mathematical modulus operation, but behaves as Java's or C's integer division.
         Both operations have the same priority that is higher than *.;
   variables 
       i : int;
       j : int;
   
   partial functions 
       . / . : int × int → int prio 11 right with λ i, j. j ≠ 0;
       . % . : int × int → int prio 11 right with λ i, j. j ≠ 0;
   
   
   axioms 
      Div-def: 0 ≤ i ∧ 0 < j → i / j * j ≤ i ∧ i < (i / j)+1 * j;
      
      Div-left: j ≠ 0 → ~ i / j = ~(i / j);
      used for: s, ls;
      
      Div-right: j ≠ 0 → i / ~ j = ~(i / j);
      used for: s, ls;
      
      Mod-def: j ≠ 0 → i = i / j * j + i % j;
   
   
end enrich