CODEWITHSUNDEEP
dafnyformal-verification
Joshua Kalejaiye
Joshua Kalejaiye

Reputation: 53

Is it possible to call a function inside of a constructor in dafny?

I'm trying to flip a boolean when instantiating a class. But I'm getting the following error: " in the first division of the constructor body (before 'new;'), 'this' can only be used to assign to its fieldsResolver ".

Is this really not possible? this seems quite basic.

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;
    }

Upvotes: 2

Views: 349

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

I can't try it myself because you didn't include a complete example, but I believe you just need to add the line new; before openReservedCarPark();.

See Two-phased constructors for more details.

Upvotes: 1

Related Questions