Übereinstimmungsfehler beim Beenden der Funktion in Stainless

Question

Ich habe diesen Code, der die Beendigung eines Sortieralgorithmus in Stainless/Leon beweist. Beachten Sie, dass die verwendeten Ranking-Funktionen oder Maßnahmen nicht die richtigen sind, da dies aus einer Hausaufgabe stammt.

import stainless.lang._ 
import stainless.collection._ 


object QuickSort { 

    def isSorted(list: List[BigInt]): Boolean = list match { 
    case Cons(x, xs @ Cons(y, _)) => x <= y && isSorted(xs) 
    case _ => true 
    } 

    def quickSort(list: List[BigInt]): List[BigInt] = { 
    decreases((list.size,0)) 
    list match { 
     case Nil() => Nil[BigInt]() 
     case Cons(x, xs) => par(x, Nil(), Nil(), xs) 
    } 
    } ensuring { res => isSorted(res) } 

    def par(x: BigInt, l: List[BigInt], r: List[BigInt], ls: List[BigInt]): List[BigInt] = { 
    decreases((l.size,l.size)) 
    ls match { 
     case Nil() => quickSort(l) ++ Cons(x, quickSort(r)) 
     case Cons(x2, xs2) => if (x2 <= x) par(x, Cons(x2, l), r, xs2) else par(x, l, Cons(x2, r), xs2) 
    } 
    } 
} 

Mit diesem Code ich folgende Fehlermeldung erhalten (was ich würde sagen, dass aus dem scala Frontend kommt):

[ Error ] exercise.scala:14:5: error: overloaded method value decreases with alternatives: 
[ Error ] (rank: (Int, Int, Int, Int, Int))Unit <and> 
[ Error ] (rank: (Int, Int, Int, Int))Unit <and> 
[ Error ] (rank: (Int, Int, Int))Unit <and> 
[ Error ] (rank: (Int, Int))Unit <and> 
[ Error ] (rank: Int)Unit <and> 
[ Error ] (rank: (BigInt, BigInt, BigInt, BigInt, BigInt))Unit <and> 
[ Error ] (rank: (BigInt, BigInt, BigInt, BigInt))Unit <and> 
[ Error ] (rank: (BigInt, BigInt, BigInt))Unit <and> 
[ Error ] (rank: (BigInt, BigInt))Unit <and> 
[ Error ] (rank: BigInt)Unit 
[ Error ] cannot be applied to ((BigInt, Int)) 
       decreases((list.size,0)) 
      ^

Ich auch import scala.BigInt._ und verwandeln decreases((list.size,0)) in decreases((list.size,BigInt(0))). Schließlich ergibt dies die folgende Ausnahme (die aus dem nichtrost/inox Teil kommt):

Exception in thread "main" scala.MatchError: <untyped> (of class inox.ast.Types$Untyped$) 
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:139) 
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:115) 
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:114) 
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) 
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) 
    at scala.collection.immutable.List.foreach(List.scala:381) 
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234) 
    at scala.collection.immutable.List.map(List.scala:285) 
    at inox.ast.TreeTransformer$class.transform(TreeOps.scala:114) 
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:149) 
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:115) 
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:114) 
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) 
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) 
    at scala.collection.immutable.List.foreach(List.scala:381) 
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234) 
    at scala.collection.immutable.List.map(List.scala:285) 
    at inox.ast.TreeTransformer$class.transform(TreeOps.scala:114) 
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:149) 
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:115) 
    at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:114) 
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) 
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) 
    at scala.collection.immutable.List.foreach(List.scala:381) 
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234) 
    at scala.collection.immutable.List.map(List.scala:285) 
    at inox.ast.TreeTransformer$class.transform(TreeOps.scala:114) 
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:149) 
    at inox.ast.TreeTransformer$class.transform(TreeOps.scala:185) 
    at stainless.extraction.oo.MethodLifting$BaseTransformer$1.transform(MethodLifting.scala:133) 
    at stainless.extraction.oo.MethodLifting$$anonfun$38.apply(MethodLifting.scala:285) 
    at stainless.extraction.oo.MethodLifting$$anonfun$38.apply(MethodLifting.scala:281) 
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) 
    at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234) 
    at scala.collection.Iterator$class.foreach(Iterator.scala:893) 
    at scala.collection.AbstractIterator.foreach(Iterator.scala:1336) 
    at scala.collection.MapLike$DefaultValuesIterable.foreach(MapLike.scala:206) 
    at scala.collection.TraversableLike$class.map(TraversableLike.scala:234) 
    at scala.collection.AbstractTraversable.map(Traversable.scala:104) 
    at stainless.extraction.oo.MethodLifting$class.transform(MethodLifting.scala:281) 
    at stainless.extraction.oo.package$extractor$.transform(package.scala:16) 
    at stainless.extraction.oo.package$extractor$.transform(package.scala:16) 
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262) 
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262) 
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262) 
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262) 
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262) 
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262) 
    at inox.ast.SymbolTransformer$$anon$3.transform(TreeOps.scala:262) 
    at inox.Program$$anon$2.<init>(Program.scala:78) 
    at inox.Program$class.transform(Program.scala:76) 
    at stainless.frontends.scalac.CodeExtraction$Extraction$$anon$1.transform(CodeExtraction.scala:187) 
    at stainless.SimpleComponent$class.extract(Component.scala:46) 
    at stainless.termination.TerminationComponent$.extract(TerminationComponent.scala:8) 
    at stainless.SimpleComponent$class.apply(Component.scala:50) 
    at stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:8) 
    at stainless.MainHelpers$$anonfun$main$1.apply(MainHelpers.scala:76) 
    at stainless.MainHelpers$$anonfun$main$1.apply(MainHelpers.scala:76) 
    at scala.collection.immutable.List.foreach(List.scala:381) 
    at stainless.MainHelpers$class.main(MainHelpers.scala:76) 
    at stainless.Main$.main(Main.scala:5) 
    at stainless.Main.main(Main.scala) 

Alle Ideen, warum dies geschieht und wie kann ich es lösen? Ich habe auch versucht, decreases(list.size,BigInt(0)) und mehrere andere Versionen zu nennen, und es hat nicht funktioniert.

bearbeiten

offenbar die Linie zu entfernen import scala.BigInt._ löst das Problem so eine Ahnung, warum dies geschieht?

Answer 1

Die Art, wie Stainless seine Bäume aus dem Scalac-Frontend extrahiert, erwartet eine bestimmte Baumstruktur für die BigInt-Extraktion. Diese Struktur ist etwas anders, wenn BigInt(_) von scala.BigInt._ importiert wird.

Dies macht nicht viel Sinn und kann durch die Verwendung von Symbolen anstelle von exakter Baumanpassung vermieden werden. Ich werde das Problem beheben.