Example #2
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
This code is not correct. Plain precondition on dispatching subprogram is
not allowed in SPARK. Otherwise it would have to be both weaker and
stronger than the class-wide precondition (because they are both checked
dynamically on both plain calls and dispatching calls).
Plain postcondition is allowed, and should be stronger than class-wide
postcondition (plain postcondition used for plain calls).
Example #3
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
This code is correct. Class-wide precondition of Int.Bump
is inherited
by Approx_Int.Bump
. Class-wide postcondition of Approx_Int.Bump
is
stronger than the one of Int.Bump
.
Example #4
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
This code is not correct. A type must be declared abstract or "+"
overridden.
Example #5
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
This code is not correct. A type must be declared abstract or Reset
overridden Reset
is subject to Extensions_Visible
False
.
Example #6
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
This code is not correct. High: extension of Arg
is not initialized in
Reset
.
Example #7
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
This code is correct. Redispatching ensures that Arg
is fully
initialized on return.
Example #8
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
package body File_System is
procedure Create (F : out File) is
begin
F.Closed := True;
F.Is_Open := False;
end Create;
procedure Open_Read (F : in out File) is
begin
F.Is_Open := True;
end Open_Read;
procedure Close (F : in out File) is
begin
F.Closed := True;
end Close;
end File_System;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
with File_System; use File_System;
procedure OO_Example_08 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_08;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package body File_System is
procedure Create (F : out File) is
begin
F.Closed := True;
F.Is_Open := False;
end Create;
procedure Open_Read (F : in out File) is
begin
F.Is_Open := True;
end Open_Read;
procedure Close (F : in out File) is
begin
F.Closed := True;
end Close;
end File_System;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
This code is correct. State automaton encoded in class-wide contracts is
respected.
Example #9
package File_System.Sync is
type File is new File_System.File with private;
function Is_Synchronized (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open and F.Is_Synchronized;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open and F.Is_Synchronized,
Post'Class => F.Closed;
private
type File is new File_System.File with record
In_Synch : Boolean := True;
end record;
function Is_Synchronized (F : File) return Boolean is
(F.In_Synch);
end File_System.Sync;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package body File_System is
procedure Create (F : out File) is
begin
F.Closed := True;
F.Is_Open := False;
end Create;
procedure Open_Read (F : in out File) is
begin
F.Is_Open := True;
end Open_Read;
procedure Close (F : in out File) is
begin
F.Closed := True;
end Close;
end File_System;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
with File_System; use File_System;
procedure OO_Example_08 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_08;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
package body File_System.Sync is
procedure Create (F : out File) is
begin
File_System.File (F).Create;
F.In_Synch := True;
end Create;
procedure Open_Read (F : in out File) is
begin
File_System.File (F).Open_Read;
F.In_Synch := True;
end Open_Read;
procedure Close (F : in out File) is
begin
File_System.File (F).Close;
F.Closed := True;
end Close;
end File_System.Sync;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package body File_System is
procedure Create (F : out File) is
begin
F.Closed := True;
F.Is_Open := False;
end Create;
procedure Open_Read (F : in out File) is
begin
F.Is_Open := True;
end Open_Read;
procedure Close (F : in out File) is
begin
F.Closed := True;
end Close;
end File_System;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package File_System.Sync is
type File is new File_System.File with private;
function Is_Synchronized (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open and F.Is_Synchronized;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open and F.Is_Synchronized,
Post'Class => F.Closed;
private
type File is new File_System.File with record
In_Synch : Boolean := True;
end record;
function Is_Synchronized (F : File) return Boolean is
(F.In_Synch);
end File_System.Sync;
with File_System; use File_System;
procedure OO_Example_08 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_08;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
with File_System.Sync; use File_System.Sync;
procedure OO_Example_09 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_09;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package body File_System is
procedure Create (F : out File) is
begin
F.Closed := True;
F.Is_Open := False;
end Create;
procedure Open_Read (F : in out File) is
begin
F.Is_Open := True;
end Open_Read;
procedure Close (F : in out File) is
begin
F.Closed := True;
end Close;
end File_System;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package File_System.Sync is
type File is new File_System.File with private;
function Is_Synchronized (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open and F.Is_Synchronized;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open and F.Is_Synchronized,
Post'Class => F.Closed;
private
type File is new File_System.File with record
In_Synch : Boolean := True;
end record;
function Is_Synchronized (F : File) return Boolean is
(F.In_Synch);
end File_System.Sync;
with File_System; use File_System;
procedure OO_Example_08 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_08;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
package body File_System.Sync is
procedure Create (F : out File) is
begin
File_System.File (F).Create;
F.In_Synch := True;
end Create;
procedure Open_Read (F : in out File) is
begin
File_System.File (F).Open_Read;
F.In_Synch := True;
end Open_Read;
procedure Close (F : in out File) is
begin
File_System.File (F).Close;
F.Closed := True;
end Close;
end File_System.Sync;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
This code is not correct. Medium: class-wide precondition might be
stronger than overridden one
Example #10
package File_System.Sync is
type File is new File_System.File with private;
function Is_Synchronized (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is new File_System.File with record
In_Synch : Boolean;
end record with
Predicate => File_System.File (File).Closed
or In_Synch;
function Is_Synchronized (F : File) return Boolean is
(F.In_Synch);
end File_System.Sync;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package body File_System is
procedure Create (F : out File) is
begin
F.Closed := True;
F.Is_Open := False;
end Create;
procedure Open_Read (F : in out File) is
begin
F.Is_Open := True;
end Open_Read;
procedure Close (F : in out File) is
begin
F.Closed := True;
end Close;
end File_System;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
with File_System; use File_System;
procedure OO_Example_08 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_08;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
package body File_System.Sync is
procedure Create (F : out File) is
begin
File_System.File (F).Create;
F.In_Synch := True;
end Create;
procedure Open_Read (F : in out File) is
begin
File_System.File (F).Open_Read;
F.In_Synch := True;
end Open_Read;
procedure Close (F : in out File) is
begin
File_System.File (F).Close;
F.Closed := True;
end Close;
end File_System.Sync;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
with File_System.Sync; use File_System.Sync;
procedure OO_Example_09 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_09;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
package body File_System.Sync is
procedure Create (F : out File) is
begin
File_System.File (F).Create;
F.In_Synch := True;
end Create;
procedure Open_Read (F : in out File) is
begin
File_System.File (F).Open_Read;
F.In_Synch := True;
end Open_Read;
procedure Close (F : in out File) is
begin
File_System.File (F).Close;
F.Closed := True;
end Close;
end File_System.Sync;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package body File_System is
procedure Create (F : out File) is
begin
F.Closed := True;
F.Is_Open := False;
end Create;
procedure Open_Read (F : in out File) is
begin
F.Is_Open := True;
end Open_Read;
procedure Close (F : in out File) is
begin
F.Closed := True;
end Close;
end File_System;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package File_System.Sync is
type File is new File_System.File with private;
function Is_Synchronized (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is new File_System.File with record
In_Synch : Boolean;
end record with
Predicate => File_System.File (File).Closed
or In_Synch;
function Is_Synchronized (F : File) return Boolean is
(F.In_Synch);
end File_System.Sync;
with File_System; use File_System;
procedure OO_Example_08 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_08;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
with File_System.Sync; use File_System.Sync;
procedure OO_Example_09 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_09;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
with File_System.Sync; use File_System.Sync;
procedure OO_Example_10 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_10;
package Show_Contract_Override is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class uses Approx_Int.Small
-- inherited Post'Class uses Approx_Int.Get_Value
end Show_Contract_Override;
package body OO_Example_07 is
function Zero return Int is
((0, 0, 0));
procedure Reset (Arg : out Int) is
begin
Int'Class (Arg) := Zero;
end Reset;
function Zero return Approx_Int is
((0, 0, 0, 0));
end OO_Example_07;
package body File_System is
procedure Create (F : out File) is
begin
F.Closed := True;
F.Is_Open := False;
end Create;
procedure Open_Read (F : in out File) is
begin
F.Is_Open := True;
end Open_Read;
procedure Close (F : in out File) is
begin
F.Closed := True;
end Close;
end File_System;
package OO_Example_03 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int) with
Post'Class => Arg.Value = Arg.Value'Old + 10;
end OO_Example_03;
procedure Show_Trivial_Example is
package Pkg_Trivial is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) is null;
end Pkg_Trivial;
use Pkg_Trivial;
procedure Call_Bump
(Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Trivial_Example;
with Show_LSP; use Show_LSP;
procedure Show_Dynamic_Dispatching_Verification is
procedure Call_Bump (Arg : in out Int'Class) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old
is
begin
Arg.Bump;
end Call_Bump;
begin
null;
end Show_Dynamic_Dispatching_Verification;
package OO_Example_07 is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Zero return Int;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
overriding function Zero return Approx_Int;
-- inherited procedure Reset
end OO_Example_07;
package File_System is
type File is tagged private;
function Closed (F : File) return Boolean;
function Is_Open (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is tagged record
Closed : Boolean := True;
Is_Open : Boolean := False;
end record;
function Closed (F : File) return Boolean is
(F.Closed);
function Is_Open (F : File) return Boolean is
(F.Is_Open);
end File_System;
package body OO_Example_03 is
procedure Bump (Arg : in out Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Arg.Value := Arg.Value + 10;
end Bump;
end OO_Example_03;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Dynamic_Dispatching is
I : Int;
AI : Approx_Int;
begin
declare
IC : Int'Class := Int'Class (I);
begin
IC.Bump; -- call to Int.Bump
end;
declare
IC : Int'Class := Int'Class (AI);
begin
IC.Bump; -- call to Approx_Int.Bump
end;
end Use_Dynamic_Dispatching;
package Show_Derived_Methods is
pragma Elaborate_Body;
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean;
overriding procedure Bump (Arg : in out Approx_Int);
not overriding procedure Blur (Arg : in out Approx_Int);
end Show_Derived_Methods;
package Show_LSP is
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
type Approx_Int is new Int with record
Precision : Natural := 0;
end record;
overriding procedure Bump (Arg : in out Approx_Int);
-- inherited Pre'Class from Int.Bump
-- inherited Post'Class from Int.Bump
end Show_LSP;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Derived_Methods is
I : Int;
AI : Approx_Int;
begin
Bump (I); -- call to Int.Bump
I.Bump; -- call to Int.Bump (object.method notation)
Bump (AI); -- call to Approx_Int.Bump
Bump (Int (AI)); -- call to Int.Bump
end Use_Derived_Methods;
package Show_Type_Primitives is
type Int is range 1 .. 10;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Type_Primitives;
package OO_Example_04 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function "+" (Arg1, Arg2 : Int) return Int with
Pre'Class => Arg1.Min = Arg2.Min
and Arg1.Max = Arg2.Max;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited function “+”
end OO_Example_04;
package body Show_Derived_Methods is
function Equal (Arg1, Arg2 : Int) return Boolean is
(Arg1 = Arg2);
procedure Bump (Arg : in out Int) is
Next : constant Integer := (if Arg.Value < Integer'Last
then Arg.Value + 1
else Integer'Last);
begin
if Next <= Arg.Max then
Arg.Value := Next;
end if;
end Bump;
overriding function Equal (Arg1, Arg2 : Approx_Int)
return Boolean is
(Arg1 = Arg2);
overriding procedure Bump (Arg : in out Approx_Int) is
begin
Bump (Int (Arg));
end Bump;
not overriding procedure Blur (Arg : in out Approx_Int) is
Prev : constant Integer := (if Arg.Value > Integer'First
then Arg.Value - 1
else Integer'First);
begin
if Arg.Value >= Prev then
Arg.Value := Prev;
end if;
end Blur;
end Show_Derived_Methods;
package File_System.Sync is
type File is new File_System.File with private;
function Is_Synchronized (F : File) return Boolean;
procedure Create (F : out File) with
Post'Class => F.Closed;
procedure Open_Read (F : in out File) with
Pre'Class => F.Closed,
Post'Class => F.Is_Open;
procedure Close (F : in out File) with
Pre'Class => F.Is_Open,
Post'Class => F.Closed;
private
type File is new File_System.File with record
In_Synch : Boolean;
end record with
Predicate => File_System.File (File).Closed
or In_Synch;
function Is_Synchronized (F : File) return Boolean is
(F.In_Synch);
end File_System.Sync;
with File_System; use File_System;
procedure OO_Example_08 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_08;
package body OO_Example_06 is
procedure Reset (Arg : out Int) is
begin
Arg := Int'(Min => -100,
Max => 100,
Value => 0);
end Reset;
end OO_Example_06;
package OO_Example_05 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_05;
package Show_Classes is
type Int is tagged record
Min, Max, Value : Integer;
end record;
function Equal (Arg1, Arg2 : Int) return Boolean;
procedure Bump (Arg : in out Int);
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- implicit definition of Equal and Bump for Approx_Int
end Show_Classes;
with Show_Derived_Methods; use Show_Derived_Methods;
procedure Use_Classwide_Dispatching is
procedure Call_Bump (Arg : in out Int'Class) is
begin
Arg.Bump;
end Call_Bump;
I : Int;
AI : Approx_Int;
begin
Call_Bump (Int'Class (I)); -- calls Int.Bump(I)
Call_Bump (Int'Class (AI)); -- calls Approx_Int.Bump(AI)
end Use_Classwide_Dispatching;
package body File_System.Sync is
procedure Create (F : out File) is
begin
File_System.File (F).Create;
F.In_Synch := True;
end Create;
procedure Open_Read (F : in out File) is
begin
File_System.File (F).Open_Read;
F.In_Synch := True;
end Open_Read;
procedure Close (F : in out File) is
begin
File_System.File (F).Close;
F.Closed := True;
end Close;
end File_System.Sync;
with Show_Contract_Override; use Show_Contract_Override;
procedure Show_Redispatching is
procedure Re_Call_Bump (Arg : in out Int)
with Extensions_Visible is
begin
Int'Class (Arg).Bump;
end Re_Call_Bump;
begin
null;
end Show_Redispatching;
package OO_Example_06 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Reset (Arg : out Int) with Extensions_Visible;
type Approx_Int is new Int with record
Precision : Natural;
end record;
-- inherited procedure Reset
end OO_Example_06;
package OO_Example_02 is
type Int is tagged record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre => Arg.Value < Arg.Max - 10,
Post => Arg.Value > Arg.Value'Old;
end OO_Example_02;
package Show_Classwide_Contracts is
type Int is tagged private;
function Get_Value (Arg : Int) return Integer;
function Small (Arg : Int) return Boolean with Ghost;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Small,
Post'Class => Arg.Get_Value > Arg.Get_Value'Old;
private
type Int is tagged record
Min, Max, Value : Integer := 0;
end record;
function Get_Value (Arg : Int) return Integer is
(Arg.Value);
function Small (Arg : Int) return Boolean is
(Arg.Value < Arg.Max - 10);
end Show_Classwide_Contracts;
with File_System.Sync; use File_System.Sync;
procedure OO_Example_09 is
procedure Use_File_System (F : out File'Class) is
begin
F.Create;
F.Open_Read;
F.Close;
end Use_File_System;
begin
null;
end OO_Example_09;
package OO_Example_01 is
type Int is record
Min, Max, Value : Integer;
end record;
procedure Bump (Arg : in out Int) with
Pre'Class => Arg.Value < Arg.Max - 10,
Post'Class => Arg.Value > Arg.Value'Old;
end OO_Example_01;
This code is correct. Predicate encodes the additional constraint on
opened files. Type invariants are not yet supported on tagged types in
SPARK.