struct Rectangle {
	//@ ensures \result == 11;
        int area() const { return 11; }
};

struct Square : public Rectangle {
	//@ ensures \result == 22;
        int area() const { return 22; }
};