class Taxpayer {

    /* isFemale is true iff the person is female */
    var isFemale : bool;
    
    /* isMale is true iff the person is male */
    var isMale : bool;

    var father : Taxpayer; // These fields won't really be used until
    var mother : Taxpayer; // the bonus part of the exercise.

    /* Age in years */ 
    var age : nat; 

    var isMarried : bool; 
    
    /* Reference to spouce if person is married, null otherwise */
    var spouse : Taxpayer; 

    /* Constant default income tax allowance */
    static function method DEFAULT_ALLOWANCE() : int { 5000 }

    /* Constant income tax allowance for Old Age Pensioners over 65 */
    static function method ALLOWANCE_OAP() : int { 7000 }

    /* Income tax allowance */
    var tax_allowance : int; 

    /* Income per year */
    var income : int; 

    /* CLASS INVARIANTS */
    predicate InvariantsHold()
        reads this;
    {
        // insert all class invariants here
        true
    }

    predicate Valid()
        reads this, spouse, mother, father;
    {
        this.InvariantsHold() &&
        (spouse == null || spouse.InvariantsHold()) &&
        (mother == null || mother.InvariantsHold()) &&
        (father == null || father.InvariantsHold())
    }

    /* CONSTRUCTOR */
    method Init(isBoy : bool, mum: Taxpayer, dad: Taxpayer) 
        requires mum == null || mum.Valid();
        requires dad == null || dad.Valid();
        ensures Valid();
    {
        age := 0;
        isMarried := false;
        isMale := isBoy;
        isFemale := !isBoy;
        mother := mum;
        father := dad;
        spouse := null;
        income := 0;
        tax_allowance := DEFAULT_ALLOWANCE();
        /* The line below makes explicit the assumption that a new Taxpayer is not
         * married to anyone yet. A bit silly of course, but we need this to keep
         * Dafny happy. */
        assume forall t : Taxpayer :: t == null || t.spouse != this;
    } 
    
    /* METHODS */

    /* Marry to new_spouse */
    method marry(new_spouse: Taxpayer) 
        requires Valid();
        ensures Valid();
    {
        spouse := new_spouse;
        isMarried := true;
    }
 
    /* Divorce from current spouse */
    method divorce()
        requires Valid();
        ensures Valid(); 
    {
        spouse.spouse := null;
        spouse := null;
        isMarried := false;
    }

    /* Transfer change of the tax allowance from this person to his/her spouse */
    method transferAllowance(change: int)
        requires Valid();
        ensures Valid(); 
    {
        tax_allowance := tax_allowance - change;
        spouse.tax_allowance := spouse.tax_allowance + change;
    }

    /* Taxpayer has a birthday and the age increases by one */
    method haveBirthday()
        requires Valid();
        ensures Valid(); 
    {
        age := age + 1;
    }
}