dafny - 使用类时缺少程序集引用

Question

我有以下代码

class clazz
{
    constructor {:axiom} () requires true

    method su(x: int, y:int) returns (r: int) 
    {
       r := x + y;
    }
}

method {:main} Main() {
   var c := new clazz();
   var s := c.su(2,3);
   print(s);
}

如何使用clazz类？这是具体错误：

error CS1061: Type `__default.ClassRoomExample' does not contain a definition for `__ctor'and no extension method `__ctor' of type `__default.ClassRoomExample' could be found. Are you missing an assembly reference?

标签： dafny

Answer 1

我刚刚发现了问题所在。在构造函数中缺少 a { }。哑的。