在不鏽鋼中使用構造構造

我試圖在不鏽鋼中證明如果兩個列表具有相同的內容並且一個列表由x界定，那麼另一個列表也由x界定。這樣做，我被告知可以使用結構：在不鏽鋼中使用構造構造

forall(x => list.content.contains(x) ==> p(x))

引理將被寫入（在鬆散的方式）爲：

def lowerBoundLemma(l1: List[BigInt],l2: List[BigInt],x:BigInt) : Boolean = { 
    require(l1.content == l2.content && forall(y => l1.content.contains(y) ==> y <= x)) 
    forall(z => l2.content.contains(z) ==> z <= x) because{ 
     forall(z => l2.content.contains(z) ==> z <= x) ==| l1.content == l2.content | 
     forall(z => l1.content.contains(z) ==> z <= x) ==| trivial     | 
     forall(y => l1.content.contains(z) ==> y <= x) 
    } 
    }.holds

的問題是，我收到以下錯誤：

exercise.scala:12:48: error: missing parameter type 
require(l1.content == l2.content && forall(y => l1.content.contains(y) ==> y <= x))

有一次，我的類型添加到y我得到這個錯誤（指向的左括號包含括號）：

exercise.scala:12:81: error: ')' expected but '(' found. 
require(l1.content == l2.content && forall(y : BigInt => l1.content.contains(y) ==> y <= x))

任何想法爲什麼會發生這種情況？

我也嘗試過的語法l.forall(_ <= x)但與像because和類型的==|結構結合我得到的錯誤：因爲不是布爾的成員。

來源

2017-03-04 Rodrigo

您面臨的問題是來自Scala編譯器前端的不鏽鋼。在Scala中，對於一個封閉的語法（與指定的參數類型）爲(x: Type) => body（注意額外的括號！）

如果你想使用because和==|，你必須在你的源文件的開頭添加import stainless.proof._ 。

來源

2017-03-04 13:36:21

在不鏽鋼中使用構造構造

回答

相關問題