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 * (unfortunately,
         this does not conform to school mathematics).
         For German speakers: Bruch = fraction, Zaehler = numerator, Nenner = denominator;

   
   
   functions  . / . : int × int → int prio 11 right;
              . % . : int × int → int prio 11 right;
   
   
   
   
   

   

   axioms Div-def :  ⊦ 0 ≤ i ∧ 0 < j → i / j * j ≤ i ∧ i < (i / j)+1 * j;
          used for: nokodkodax;
          Div-left :  ⊦ j ≠ 0 → ~ i / j = ~(i / j);
          used for: s, ls, nokodkodax;
          Div-right :  ⊦ j ≠ 0 → i / ~ j = ~(i / j);
          used for: s, ls, nokodkodax;
          Mod-def :  ⊦ j ≠ 0 → i = i / j * j + i % j;
          used for: nokodkodax;

   

   
end enrich