VHDL Issue Number:      1083
Classification:         Language Definition Problem
Language Version:       VHDL-93
Summary:                Pureness of function ENDFILE
Related Issues:
Relevant LRM Sections:  2.1  2.1.1.3  2.2  3.4.1
Key Words and Phrases:  pure function, file
Current Status:         ISAC-Approved
1076-1993 Disposition:  N/A
Disposition Rationale:  N/A
Superseded By:          N/A
-----------------------
Date Submitted:         1994/03/22
Author of Submission:   Anne Robert
Author's Affiliation:   LEDA S.A.
Author's Post Address:  35 Av du Granier
                        38240 MEYLAN
                        FRANCE
Author's Phone Number:  (+33) 76 41 92 43
Author's Fax Number:    (+33) 76 41 92 44
Author's Net Address:   anee@leda.fr
-----------------------
Date Analyzed:          1994/03/26
Author of Analysis:     Andy Tsay (Fintronic USA)
Revision Number:        $Revision: 1.3 $
Date Last Revised:      $Date: 1995/04/14 00:08:59 $


Description of Problem
----------------------
LRM 2.1 says "A function is impure if its specification contains the
reserved word IMPURE; otherwise, it is said to be pure."

File operations are described in LRM 3.4.1:

   The language implicitly defines the operations for objects of a
   file type.
   ...
   function ENDFILE (file F: FT) return BOOLEAN;

According to above statements, function ENDFILE is a pure function.
But according to LRM 2.2:

   A pure function must not contain a reference to an explicitly declared
   file object.

Should this imply that a pure function may not have a file parameter?
In this case the function ENDFILE should be impure and not pure.

Proposed Resolution
-------------------
Make explicit that a pure function cannot have a file parameter.


VASG-ISAC Analysis & Rationale
------------------------------
There appears to be consensus that:

1.  ENDFILE is an impure function, and
2.  that pure functions should not have access to files.

ENDFILE is an impure function because it has to refer to the file parameter
to check the end of file condition. LRM 2.1.1.3 states that a reference to
the formal (file) parameter must be equivalent to a reference to the actual
parameter. LRM does not disallow file parameters and file declarations in a
pure function.

There was some debate about how to best implement the second item of
consensus.  The two choices are:

1.  Add the restriction that pure functions may not have file parameters.
2.  Disallow the occurrence of file operations from within the bodies of pure
functions.

It was observed that approach 1 does not require the analysis of the
subprogram body to detect the error, while approach 2 requires analysis of the
function's body.  Based on this observation, consensus was quickly reached on
the first approach.

A subsidiary question was: "Can a pure function declare a file object within
it's body?"  Although it appears that it can, it is clear that it cannot be
referenced and therefore cannot be used.  It seems worth disallowing this case
for pure functions, since a pure function could otherwise be written that can
query the existence of external files.

It also appears that there is another potential hole.  A pure function
declared within an impure function could reference a file parameter of the
impure function.  This case should also be disallowed.

There was some discussion as to whether asserts should be disallowed in pure
functions.  After some discussion, the consensus seemed to be that they should
continue to be allowed.


VASG-ISAC Recommendation for IEEE Std 1076-1993
-----------------------------------------------
Make the following two modifications to the '93 LRM:

   1. add keyword impure to ENDFILE declaration in LRM 3.4.1:
      Replace the following declaration

                 function ENDFILE (file F: FT) return BOOLEAN;

      with the new declaration

          impure function ENDFILE (file F: FT) return BOOLEAN;
          ------

   2. add restrictions to the pure function in LRM 2.2:

      Change the following sentence

          A pure function must not contain a reference to an explicitly
          declared file object.

      to the new sentence

          A pure function must not contain any file parameter, any file
          declaration, or any reference to a file parameter or an explicitly
          declared file object.

VASG-ISAC Recommendation for Future Revisions
---------------------------------------------
TBD