Тип Square
В типе Square, предположительно являющемся подтипом Rectangle, аксиомы gw_sh и gh_sw имеют смысл, строго противоположный смыслу аналогичных аксиом в Rectangle: ---- File:./rsl/square.rsl scheme Square = class type Figure, UReal = {| r: Real :- r > 0.0 |} value SetWidth : Figure >< UReal -> Figure, SetHeight : Figure >< UReal -> Figure, GetWidth : Figure -> UReal, GetHeight : Figure -> UReal axiom [gw_sw] all w: UReal, f: Figure:- GetWidth(SetWidth(f, w))= w, [gw_sh] all h: UReal, f: Figure:- GetWidth(SetHeight(f, h)) = h, [gh_sh] all h: UReal, f: Figure:- GetHeight(SetHeight(f, h)) = h, [gh_sw] all w: UReal, f: Figure:- GetHeight(SetWidth(f, w)) = w end ---- End Of File:./rsl/square.rsl Вот аппликативная реализаци типа Square, записанная в форме наследования: ---- File:./rsl/as.rsl AR scheme AS = extend hide SetWidth, SetHeight in AR with class value SetWidth : Figure >< UReal -> Figure SetWidth ((h, w), v) is (v, v), SetHeight : Figure >< UReal -> Figure SetHeight ((h, w), v) is (v, v) end ---- End Of File:./rsl/as.rsl
В новом классе AS "наследуется" (extend) все из класса AR, но при этом "прячутся" (hide) родительские функции SetWidth, SetHeight и объявляются свои.
