Можно ли вызвать функцию внутри конструктора в 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;
    }