Làm thế nào để chứng minh kích thước của một danh sách trong Leon?

Question

Tôi đang cố gắng chứng minh rằng kích thước (số phần tử) trong một danh sách là không âm, nhưng Leon không chứng minh được nó --- nó chỉ là thời gian. Liệu Leon có thực sự không có khả năng chứng minh tài sản này, hay tôi đang sử dụng nó sai? Điểm xuất phát của tôi là một chức năng tôi đọc trong bài báo "Tổng quan về hệ thống xác minh Leon".

import leon.lang._ 
import leon.annotation._ 

object ListSize { 
    sealed abstract class List 
    case class Cons(head: Int, tail: List) extends List 
    case object Nil extends List 

    def size(l: List) : Int = (l match { 
    case Nil => 0 
    case Cons(_, t) => 1 + size(t) 
    }) ensuring(_ >= 0) 
} 

Answer 1

Phiên bản trước của Leon được xử lý Scala's Int loại là toán học, không bị chặn, số nguyên. Các phiên bản gần đây nhất xử lý các giá trị của Int dưới dạng vectơ 32 bit đã ký và yêu cầu sử dụng BigInt để biểu thị các số nguyên không bị chặn.

Trong ví dụ được cung cấp, Leon cố gắng xây dựng một danh sách có kích thước Int.MaxValue, một ví dụ phản biện chứng minh rằng điều kiện không giữ cho các số nguyên bị chặn.

Nếu bạn thay đổi loại trả lại là size thành BigInt, chương trình sẽ xác minh như mong đợi.