ContractLoadingTests

4

tests

0

failures

0

ignored

12.378s

duration

100%

successful

Tests

Test Duration Result
issues1658() 2.693s passed
specMathBigintMathTest() 3.970s passed
specMathJavaMathTest() 2.953s passed
sumAndMax() 2.762s passed

Standard output

721035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java 
721035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.2ns 
721035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721145     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
721145     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
721145     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
721145     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
721551     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
722802     DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
724992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.95s 
724992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java 
724992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms 
724992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
727743     INFO  Test worker     d.u.i.k.s.n.ContractLoadingTests self.sumAndMax(a) catch(exc)
pre: (  \forall int i;
     (   (0 <= i & i < a.length)<<SC>> & inInt(i)
      -> 0 <= a[i])
 & ((self.<inv><<impl>> & (!a = null)<<impl>>)<<SC>>))<<SC>>
post:   (\forall int i;
     (   (0 <= i & i < a.length)<<SC>> & inInt(i)
      -> a[i] <= self.max)
& ((  (   a.length >  0
       -> \exists int i;
            ((  (0 <= i
              & i < a.length)<<SC>>
              & inInt(i)
              & self.max = a[i])<<SC>>))
    & ((  self.sum = bsum{int i;}(0, a.length, a[i])
        & ((  self.sum <= a.length * self.max
            & self.<inv><<impl>>)<<SC>>))<<SC>>))<<SC>>))<<SC>>
& (exc = null)<<impl>>
mod:      {(self, SumAndMax::$sum)}
\cup {(self, SumAndMax::$max)}
termination: diamond 
727758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java 
727758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.3ns 
727758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
730463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java 
730463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.6ns 
730463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731401     DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
733402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s