OneHiveRule's questions

Dafny 有以下几种方式来声明支持相等的类型。

T(==)

但是有没有办法指定类型支持排序（<, <=, >, >=）等？

在下面的代码中，一个SomeClass对象的作用域位于一个块内，但对它的引用存储在p外部块中。稍后使用p，调用SomeMethod()of 。SomeClass

SomeClass TestMethod(SomeClass c) {
    SomeClass * p;
    {
        SomeClass t;
        p = &t;
    }
    p->SomeMethod();
    return *p;
}

是否会p->SomeMethod()因空指针取消引用而导致故障？

我尝试使用int代替SomeClass，但没有得到空指针取消引用。但我想根据 C++ 标准了解行为。