/usr/share/doc/libaunit-doc/examples/liskov/tested_lib/src/shape.ads is in libaunit-doc 3.7.2-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 | --
-- Copyright (C) 2008, AdaCore
--
package Shape is
type Shape_Type is abstract tagged private;
type Shape_Access is access all Shape_Type'Class;
-- Additional functional API for expressing pre/postconditions
-- & invariants:
-- function New_Shape (W, H : Natural) return Shape;
-- function Set_Width (S : Shape; W : Natural) return Shape;
-- function Set_Height (S : Shape; H : Natural) return Shape;
--
-- Class invariants:
-- for_all W, H in Natural:
-- Set_Width (New_Shape (W, H), X) = New_Shape (X, H))
-- Set_Height (New_Shape (W, H), X) = New_Shape (W, X))
function Width (Obj : Shape_Type) return Natural;
function Height (Obj : Shape_Type) return Natural;
procedure Set_Width (Obj : in out Shape_Type; W : Natural);
-- pragma Postcondition
-- (Width (Obj) = W -- expected result
-- and Height (Obj) = Height (Obj'Old) -- independence
-- );
procedure Set_Height (Obj : in out Shape_Type; H : Natural);
-- pragma Postcondition
-- (Height (Obj) = H -- expected result
-- and Width (Obj) = Width (Obj'Old) -- independence
-- );
function Area (Obj : Shape_Type) return Natural is abstract;
private
type Shape_Type is abstract tagged record
Width : Natural;
Height : Natural;
end record;
end Shape;
|