[Ada] Aspect Refined_Post

[Arnaud Charlet <charlet at adacore dot com>]

This patch provides the initial implementation of aspect/pragma Refined_Post.
This construct is intended for formal verification proofs.

The syntax of the aspect is as follows:

   ASPECT_DEFINITION ::= ( boolean_EXPRESSION )

The syntax of the pragma is as follows:

   pragma Refined_Post ( boolean_EXPRESSION );

The semantic rules of this construct are:

A Refined_Post aspect may only appear on a body_stub (if one is present) or the
body (if no stub is present) of a subprogram which is declared in the visible
part of a package.

The same legality rules apply to a Refined Postcondition as for a postcondition.

A Refined Postcondition of a subprogram defines a refinement of the
postcondition of the subprogram.

Logically, the Refined Postcondition of a subprogram must imply its
postcondition. This means that it is perfectly logical for the declaration not
to have a postcondition (which in its absence defaults to True) but for the
body or body stub to have a Refined Postcondition.

For an expression_function without an explicit Refined Postcondition the
expression implementing the function acts as its Refined Postcondition.

The static semantics are otherwise as for a postcondition.

When a subprogram with a Refined Postcondition is called; first the subprogram
is evaluated. The Refined Postcondition is evaluated immediately before the
evaluation of the postcondition or, if there is no postcondition, immediately
before the point at which a postcondition would have been evaluated. If the
Refined Postcondition evaluates to True then the postcondition is evaluated as
described in the Ada RM. If either the Refined Postcondition or the
postcondition do not evaluate to True then the exception
Assertions.Assertion_Error is raised.

-------------
-- Sources --
-------------

--  semantics.ads

package Semantics is
   procedure OK_1 (Formal : out Integer)
     with Post => Formal > 12;

   procedure OK_2 (Formal : out Integer);
   procedure OK_3 (Formal : out Integer);
   procedure OK_4 (Formal : out Integer);
   function  OK_5 (Formal : Integer) return Integer;
   procedure OK_6 (Formal : out Integer);
   procedure Error_1 (Formal : out Integer);
   procedure Error_2 (Formal : out Integer);
   procedure Error_3 (Formal : out Integer);
   function  Error_9 (Formal : Integer) return Integer is  --  not in body
     (Formal * Formal) with Refined_Post => Error_9'Result > 12;
end Semantics;

--  semantics.adb

package body Semantics is
   Local : Integer;

   procedure OK_1 (Formal : out Integer)
     with Refined_Post => Formal + Local > 34 is
   begin null; end OK_1;

   procedure OK_2 (Formal : out Integer)
     with Refined_Post => Formal + Local > 34 is
   begin null; end OK_2;

   procedure OK_3 (Formal : out Integer) is separate
     with Refined_Post => Formal + Local > 34;

   procedure OK_4 (Formal : out Integer) is separate;
   pragma Refined_Post (Formal + Local > 34);

   package Nested_OK is
      procedure OK_4 (Formal : out Integer);
   end Nested_OK;

   package body Nested_OK is
      procedure OK_4 (Formal : out Integer)
        with Refined_Post => Formal + Local > 34 is
      begin null; end OK_4;
   end Nested_OK;

   function OK_5 (Formal : Integer) return Integer is
     (Formal * Local) with Refined_Post => OK_5'Result > 34;

   procedure OK_6 (Formal : out Integer) is separate;

   procedure Error_1 (Formal : out Integer)
     with Refined_Post => Local is  --  expression must be boolean
   begin null; end Error_1;

   procedure Error_2 (Formal : out Integer) is separate  --  expression must be
     with Refined_Post => Formal + 1;                    --  boolean, no body

   procedure Error_3 (Formal : out Integer) is separate;
   pragma Refined_Post (Formal + 1);  --  expression must be boolean, no body

   procedure Error_4 (Formal : out Integer);
   procedure Error_4 (Formal : out Integer)
     with Refined_Post => Formal + Local > 654 is  --  spec is not visible
   begin null; end Error_4;

   procedure Error_5 (Formal : out Integer)
     with Refined_Post => Formal > 321 is  --  stand alone body
   begin null; end Error_5;

   package Nested_Error is
   private
      procedure Error_6 (Formal : out Integer);
   end Nested_Error;

   package body Nested_Error is
      procedure Error_6 (Formal : out Integer)
        with Refined_Post => Formal + Local > 34 is  --  spec is not visible
      begin null; end Error_6;
   end Nested_Error;

   function Error_7 (Formal : Integer) return Integer is  --  stand alone body
     (Formal * Local) with Refined_Post => Error_7'Result > 34;

   function Error_8 (Formal : Integer) return Integer;
   function Error_8 (Formal : Integer) return Integer is  --  spec not visible
     (Formal * Local) with Refined_Post => Error_8'Result > 34;
end Semantics;

--  semantics-ok_3.adb

separate (Semantics)

procedure OK_3 (Formal : out Integer) is begin null; end OK_3;

--  semantics-ok_4.adb

separate (Semantics)

procedure OK_4 (Formal : out Integer) is begin null; end OK_4;

--  semantics-ok_6.adb

separate (Semantics)

procedure OK_6 (Formal : out Integer)
  with Refined_Post => (Formal + Local > 34)
is begin null; end OK_6;

--  dynamic_semantics.ads

package Dynamic_Semantics is
   function Fail (Formal : Integer) return Integer
     with      Post => Fail'Result > 20;
   --  Refined_Post => Fail'Result > 10

   function Fail_Stub (Formal : Integer) return Integer
     with      Post => Fail_Stub'Result > 20;
   --  Refined_Post => Fail_Stub'Result > 10

   function Fail_Stub_2 (Formal : Integer) return Integer
     with      Post => Fail_Stub_2'Result > 20;
   --  Refined_Post => Fail_Stub_2'Result > 10

   procedure Set_Local (Val : Integer);
end Dynamic_Semantics;

--  dynamic_semantics.adb

with Ada.Text_IO; use Ada.Text_IO;

package body Dynamic_Semantics is
   Local : Integer := 0;

   function Fail (Formal : Integer) return Integer
     with Refined_Post => Fail'Result > 10 is
   begin
      return Formal + 1;
   end Fail;

   function Fail_Stub (Formal : Integer) return Integer is separate
     with Refined_Post => Fail_Stub'Result > 10;

   function Fail_Stub_2 (Formal : Integer) return Integer is separate;

   procedure Set_Local (Val : Integer) is
   begin
      Local := Val;
   end Set_Local;
end Dynamic_Semantics;

--  dynamic_semantics-fail_stub.adb

separate (Dynamic_Semantics)

function Fail_Stub (Formal : Integer) return Integer is
begin
   return Formal + 1;
end Fail_Stub;

--  dynamic_semantics-fail_stub_2.adb

separate (Dynamic_Semantics)

function Fail_Stub_2 (Formal : Integer) return Integer
  with Refined_Post => Fail_Stub_2'Result > 10 is
begin
   return Formal + 1;
end Fail_Stub_2;

--  main.adb

with Ada.Assertions;    use Ada.Assertions;
with Ada.Exceptions;    use Ada.Exceptions;
with Ada.Text_IO;       use Ada.Text_IO;
with Dynamic_Semantics; use Dynamic_Semantics;

procedure Main is
   Res : Integer;

begin
   Set_Local (10);

   begin
      Res := Fail (5);
      Put_Line ("ERROR: Refined_Post did not fail (1)");
   exception
      when E : Assertion_Error => Put_Line (Exception_Information (E));
      when others => Put_Line ("ERROR: unexpected error (1)");
   end;

   begin
      Res := Fail_Stub (5);
      Put_Line ("ERROR: Refined_Post on stub did not fail (2)");
   exception
      when E : Assertion_Error => Put_Line (Exception_Information (E));
      when others => Put_Line ("ERROR: unexpected error (2)");
   end;

   begin
      Res := Fail_Stub_2 (5);
      Put_Line ("ERROR: Refined_Post on stub did not fail (3)");
   exception
      when E : Assertion_Error => Put_Line (Exception_Information (E));
      when others => Put_Line ("ERROR: unexpected error (3)");
   end;

   Set_Local (30);

   begin
      Res := Fail (15);
      Put_Line ("ERROR: Post did not fail (4)");
   exception
      when E : Assertion_Error => Put_Line (Exception_Information (E));
      when others => Put_Line ("ERROR: unexpected error (4)");
   end;

   begin
      Res := Fail_Stub (15);
      Put_Line ("ERROR: Post on stub did not fail (5)");
   exception
      when E : Assertion_Error => Put_Line (Exception_Information (E));
      when others => Put_Line ("ERROR: unexpected error (5)");
   end;

   begin
      Res := Fail_Stub_2 (15);
      Put_Line ("ERROR: Post on stub did not fail (6)");
   exception
      when E : Assertion_Error => Put_Line (Exception_Information (E));
      when others => Put_Line ("ERROR: unexpected error (6)");
   end;
end Main;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c -gnat12 -gnata semantics.adb
$ gnatmake -q -gnat12 -gnata main.adb
$ ./main
semantics.adb:34:27: expected type "Standard.Boolean"
semantics.adb:34:27: found type "Standard.Integer"
semantics.adb:37:04: warning: subunit "Semantics.Error_2" in file
  "semantics-error_2.adb" not found
semantics.adb:38:34: expected type "Standard.Boolean"
semantics.adb:38:34: found type "Standard.Integer"
semantics.adb:40:04: warning: subunit "Semantics.Error_3" in file
  "semantics-error_3.adb" not found
semantics.adb:41:32: expected type "Standard.Boolean"
semantics.adb:41:32: found type "Standard.Integer"
semantics.adb:45:11: aspect "Refined_Post" must apply to the body of a visible
  subprogram
semantics.adb:49:11: aspect "Refined_Post" cannot apply to a stand alone body
semantics.adb:59:14: aspect "Refined_Post" must apply to the body of a visible
  subprogram
semantics.adb:64:28: aspect "Refined_Post" cannot apply to a stand alone
  expression function
semantics.adb:68:28: aspect "Refined_Post" must apply to the body of a visible
  subprogram
semantics.ads:14:29: aspect "Refined_Post" cannot apply to a stand alone
  expression function
Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Refined_Post failed at dynamic_semantics.adb:7

Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Refined_Post failed at dynamic_semantics.adb:13

Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: Refined_Post failed at dynamic_semantics-fail_stub_2.adb:4

Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from dynamic_semantics.ads:3

Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from dynamic_semantics.ads:7

Exception name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from dynamic_semantics.ads:11

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry for Aspect_Refined_Post in table
	Canonical_Aspect.
	* aspects.ads: Add an entry for Aspect_Refined_Post in tables
	Aspect_Id, Aspect_Argument, Aspect_Names, Aspect_Delay,
	Aspect_On_Body_Or_Stub_OK. Update the comment on the use of
	table Aspect_On_Body_Or_Stub_OK.
	* par-prag.adb: Add pragma Refined_Post to the list of pragmas
	that do not require special processing by the parser.
	* sem_attr.adb (Analyze_Attribute): Add special analysis for
	attributes 'Old and 'Result when code generation is disabled and
	they appear in aspect/pragma Refined_Post.
	(In_Refined_Post): New routine.
	* sem_ch6.adb (Analyze_Expression_Function): Move various
	aspects and/or pragmas that apply to an expression function to the
	corresponding spec or body.
	(Collect_Body_Postconditions): New routine.
	(Process_PPCs): Use routine Collect_Body_Postconditions
	to gather all postcondition pragmas.
	* sem_ch10.adb (Analyze_Proper_Body): Use routine
	Relocate_Pragmas_To_Body to move all source pragmas that follow
	a body stub to the proper body.
	(Move_Stub_Pragmas_To_Body): Removed.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Post.
	(Check_Aspect_At_Freeze_Point): Aspect
	Refined_Post does not need delayed processing at the freeze point.
	* sem_prag.adb: Add an entry for pragma Refined_Post in
	table Sig_Flags.
	(Analyze_Pragma): Add processing for pragma
	Refined_Post. Update the processing of pragma Refined_Pre
	to use common routine Analyze_Refined_Pre_Post.
	(Analyze_Refined_Pre_Post): New routine.
	(Relocate_Pragmas_To_Body): New routine.
	* sem_prag.ads: Table Pragma_On_Stub_OK is now known as
	Pragma_On_Body_Or_Stub_OK. Update the comment on usage of
	table Pragma_On_Body_Or_Stub_OK.
	(Relocate_Pragmas_To_Body): New routine.
	* snames.ads-tmpl: Add new predefined name for Refined_Post. Add
	new Pragma_Id for Refined_Post.

Attachment: difs
Description: Text document