ContractLoadingTests

4

tests

0

failures

0

ignored

15.238s

duration

100%

successful

Tests

Test Duration Result
issues1658() 3.331s passed
specMathBigintMathTest() 5.091s passed
specMathJavaMathTest() 3.408s passed
sumAndMax() 3.408s passed

Standard output

940380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java 
940380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.3ns 
940380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
940536     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
940536     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
940536     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
940536     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
941115     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
942428     DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
945431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 
945447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java 
945447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 696.4ns 
945447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
948824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
948855     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 
948855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java 
948855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.8ns 
948871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
952186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
952202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java 
952202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.7ns 
952202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
953281     DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
955594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.4s