Тип Rectangle
Аксиомы gw_sw и gh_sh очевидны: что положил, то и получил назад. Аксиомы gw_sh и gh_sw означают независимость высоты от ширины в значениях множества Figure, соответствующих спецификации Rectangle. Например, для любого f: Figure значения, возвращаемые функцией GetWidth не зависят от применения функции SetHight. ---- File:./rsl/rectangle.rsl scheme Rectangle = 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)) = GetWidth(f), [gh_sh] all h: UReal, f: Figure:- GetHeight(SetHeight(f, h)) = h, [gh_sw] all w: UReal, f: Figure:- GetHeight(SetWidth(f, w)) = GetHeight(f) end ---- End Of File:./rsl/rectangle.rsl
Аппликативная реализация типа Rectangle может иметь следующий вид: ---- File:./rsl/ar.rsl scheme AR = class type Figure = UReal >< UReal, UReal = {| r: Real :- r > 0.0 |} value SetWidth : Figure >< UReal -> Figure SetWidth ((h, w), v) is (h, v), SetHeight : Figure >< UReal -> Figure SetHeight ((h, w), v) is (v, w), GetWidth : Figure -> UReal GetWidth (h, w) is w, GetHeight : Figure -> UReal GetHeight (h, w) is h end ---- End Of File:./rsl/ar.rsl
Домен типа Rectangle (множество Figure) объявляется как прямое произведение UReal ? UReal, функции GetWidth и GetHeight – проекции.
