ContractLoadingTests

4

tests

0

failures

0

ignored

24.353s

duration

100%

successful

Tests

Test Duration Result
issues1658() 4.875s passed
specMathBigintMathTest() 9.126s passed
specMathJavaMathTest() 5.325s passed
sumAndMax() 5.027s passed

Standard output

1266447    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\bigint\Test.java 
1266447    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.7ns 
1266447    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1266650    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1266650    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1266650    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1266650    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1267401    DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
1269739    DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
1275516    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.07s 
1275532    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from ..\key.ui\examples\heap\vstte10_01_SumAndMax\src\SumAndMax.java 
1275532    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 620.7ns 
1275537    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1280543    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 
1280559    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 
1280559    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\issues\1658\Test.java 
1280559    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
1280559    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1285418    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.87s 
1285434    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\specMath\java\Test.java 
1285434    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.6ns 
1285434    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1287122    DEBUG Test worker     d.u.i.k.j.r.ClassPreparationMethodBuilder clPrepBuilder: Inner Class detected. Reject building class initialisation methods. 
1290759    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s