ContractLoadingTests

4

tests

0

failures

0

ignored

18.650s

duration

100%

successful

Tests

Test Duration Result
issues1658() 4.185s passed
specMathBigintMathTest() 5.721s passed
specMathJavaMathTest() 4.492s passed
sumAndMax() 4.252s passed

Standard output

1062454    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java 
1062454    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.7ns 
1062469    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1062610    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1062610    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1062610    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1062610    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1063173    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
1065037    DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
1068171    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.71s 
1068171    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java 
1068171    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 470.3ns 
1068171    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1072408    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
1072423    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 
1072423    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java 
1072423    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
1072423    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1076608    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 
1076608    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java 
1076608    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.3ns 
1076608    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1078040    DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
1081100    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.5s