是否可以在 dafny 的构造函数中调用函数？

问题描述

我试图在实例化一个类时翻转一个布尔值。但我收到以下错误： " 在构造函数体的第一部分（在 'new;' 之前），'this' 只能用于分配给它的 fieldsResolver "。

这真的不可能吗？这看起来很基本。

constructor (standard_max_length : nat,reserved_max_length :nat,buffer_parking_spots : nat,weekday : bool)
    requires buffer_parking_spots < standard_max_length
    modifies this
    {
        standard_set := {};
        reserved_set := {};

        //if its a weekend,combine reserved max with standard max. treating reserved spaces as standard.
        if ( weekday )
        {
            this.standard_max_length := standard_max_length;
            this.standard_set_length := 0;
        }
        else
        {
            this.standard_max_length := standard_max_length + reserved_max_length;
            this.standard_set_length := 0;
        }

        this.reserved_max_length := reserved_max_length;
        this.reserved_set_length := 0;

        subscriptions := {};
        this.subscription_num := 0;

        this.buffer_parking_spots := buffer_parking_spots;
        this.weekday := weekday;

        openReservedCarPark();
    }

    method openReservedCarPark()
    ensures weekday ==> reserved_car_park_open   
    {
        reserved_car_park_open := true;
    }

解决方法

我无法自己尝试，因为您没有包含完整的示例，但我相信您只需要在 new; 之前添加行 openReservedCarPark();。

有关详细信息，请参阅 Two-phased constructors。