function Is_Open (File : File_Type) return Boolean; :Text_io

function Is_Open (File : File_Type) return Boolean; :Text_io

[comicfanzine]

Can someone please show my a code in which this function is used , i'm lost , thanks .

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Simon Wright]

comicfanzine@gmail.com writes:

> Can someone please show my a code in which this function is used , i'm
> lost , thanks .

You could try googling <ada text_io is_open>; finds
http://homepage.ntlworld.com/phil.brooke/topal/hg/topal/misc.adb as the
5th or 6th hit.

Or you could help us to help you by showing us how far you've got
already; "i'm lost" isn't informative.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[comicfanzine]

Thanks fot link .

I want to create+open a file then use Is_Open , if the file have been create i  want to put some text + the value of Is_Open(should be TRUE) .

There is french in the code :

[code]WITH Ada.Text_IO ;  USE Ada.Text_IO ; 

PROCEDURE TestFichier IS

   MonFichier : File_type ; 
   
BEGIN 
   Create( MonFichier,Name => "clone.adb");
   open(MonFichier,In_file,"clone.adb") ;
    if Is_Open(MonFichier) and MonFichier = true 
    then put("Le fichier , ouvert ? : ",MonFichier);
    end if;
END TestFichier ;[/code]

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Simon Wright]

comicfanzine@gmail.com writes:

> Thanks fot link .
>
> I want to create+open a file then use Is_Open , if the file have been create i  want to put some text + the value of Is_Open(should be TRUE) .
>
> There is french in the code :
>
> [code]WITH Ada.Text_IO ;  USE Ada.Text_IO ; 
>
> PROCEDURE TestFichier IS
>
>    MonFichier : File_type ; 
>    
> BEGIN 
>    Create( MonFichier,Name => "clone.adb");
>    open(MonFichier,In_file,"clone.adb") ;
>     if Is_Open(MonFichier) and MonFichier = true 
>     then put("Le fichier , ouvert ? : ",MonFichier);
>     end if;
> END TestFichier ;[/code]

Compiling this with listing (gnatmake -gnatl testfichier.adb) gives

     3. PROCEDURE TestFichier IS
     4.
     5.    MonFichier : File_type ;
     6.    
     7. BEGIN
     8.    Create( MonFichier,Name => "clone.adb");
     9.    open(MonFichier,In_file,"clone.adb") ;
    10.     if Is_Open(MonFichier) and MonFichier = true
                                                  |
        >>> invalid operand types for operator "="
        >>> left operand has private type "Ada.Text_Io.File_Type"
        >>> right operand has type "Standard.Boolean"
    11.     then put("Le fichier , ouvert ? : ",MonFichier);
                 1   3
        >>> no candidate interpretations match the actuals:
        >>> too many arguments in call to "put"
        >>> expected private type "Ada.Text_Io.File_Type"
        >>> found a string type
        >>>   ==> in call to "Put" at a-textio.ads:241
        >>>   ==> in call to "Put" at a-textio.ads:207

    12.     end if;
    13. END TestFichier ;

First, the compiler messages:

Line 10
-------
Is_Open returns Boolean, and MonFichier is a File_Type and can't be
compared to Boolean (in fact, it's limited private, so it can't by
default be compared to anything!) so I think you just meant

   if Is_Open (MonFichier)

Line 11
-------
You have the arguments the wrong way round. You could use named
parameter association if you insist on this order,

   Put (Item => "Le fichier , ouvert ? : ", File => MonFichier);

==============================

Second, the semantic problems: Create at line 8 will either result in an
opened writable file (MonFichier) or will raise an exception if the file
already existed.

If you get to line 9 (i.e. the Create was successful) you will get an
exception because the file is already open.

If you were to get to line 10, Is_Open would have to return True.

If you were to get to line 11 having executed line 9, you would get an
exception because you opened MonFichier read-only.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[AdaMagica]

Am Montag, 26. Oktober 2015 19:02:00 UTC+1 schrieb Simon Wright:
> Second, the semantic problems: Create at line 8 will either result in an
> opened writable file (MonFichier) or will raise an exception if the file
> already existed.

A.8.2(3/2) "Establishes a new external file, ..."
(5) Doesn't mention an exception if file exists.

I interprete this as: If the file exists, a new file is created nevertheless and the old contents are lost.
So does Gnat GPL 2015.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Simon Wright]

AdaMagica <christ-usch.grein@t-online.de> writes:

> Am Montag, 26. Oktober 2015 19:02:00 UTC+1 schrieb Simon Wright:
>> Second, the semantic problems: Create at line 8 will either result in an
>> opened writable file (MonFichier) or will raise an exception if the file
>> already existed.
>
> A.8.2(3/2) "Establishes a new external file, ..."
> (5) Doesn't mention an exception if file exists.
>
> I interprete this as: If the file exists, a new file is created
> nevertheless and the old contents are lost.
> So does Gnat GPL 2015.

Quite right, sorry, I was thinking of the usual dance when you want to
write to a file whether or not it exists already.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Jeffrey R. Carter]

On 10/26/2015 06:25 AM, comicfanzine@gmail.com wrote:
> Thanks fot link .
> 
> I want to create+open a file then use Is_Open , if the file have been create i  want to put some text + the value of Is_Open(should be TRUE) .
> 
> There is french in the code :
> 
> [code]WITH Ada.Text_IO ;  USE Ada.Text_IO ; 
> 
> PROCEDURE TestFichier IS
> 
>    MonFichier : File_type ; 
>    
> BEGIN 
>    Create( MonFichier,Name => "clone.adb");
>    open(MonFichier,In_file,"clone.adb") ;

Create leaves the file open; you don't need to Open it after Create. In fact,
Open should raise Status_Error if the file is already open. See ARM A.8.2

http://www.adaic.org/resources/add_content/standards/12rm/html/RM-A-8-2.html


>     if Is_Open(MonFichier) and MonFichier = true 

Monfichier is of private type Ada.Text_IO.File_Type, and True, since you have
not defined it yourself, is of type Boolean. Since you have not defined "=" for
these 2 types, the comparison on the right of "and" will not compile. What you
want is probably

if Is_Open (Monfichier) then

[Note that Ada is case insensitive, and many of us will reformat your code for
easier reading, converting CamelCase to Camelcase in the process. This is partly
why CamelCase is not recommended for Ada, where the common usage is to separate
words with underlines, giving Mon_Fichier. Ada is also designed to read, as much
as possible, as English text, so using identifiers in another language is not a
good idea.]

>     then put("Le fichier , ouvert ? : ",MonFichier);

This also won't compile: There is no Put visible that takes a String as its 1st
parameter and a File_Type as its 2nd. Using named notation will let you put the
parameters in any order you like, and make the code easier to read:

Put (Item => "Le fichier , ouvert ? : ", File => Monfichier);

>     end if;
> END TestFichier ;[/code]
> 


-- 
Jeff Carter
"I'm a kike, a yid, a heebie, a hook nose! I'm Kosher,
Mum! I'm a Red Sea pedestrian, and proud of it!"
Monty Python's Life of Brian
77

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[comicfanzine]

Le lundi 26 octobre 2015 12:27:53 UTC+1, Simon Wright a écrit :
> comicfanzine@gmail.com writes:
> 
> > Can someone please show my a code in which this function is used , i'm
> > lost , thanks .
> 
> You could try googling <ada text_io is_open>; finds
> http://homepage.ntlworld.com/phil.brooke/topal/hg/topal/misc.adb as the
> 5th or 6th hit.
> 
> Or you could help us to help you by showing us how far you've got
> already; "i'm lost" isn't informative.

Thanks fot link .

I want to create+open a file then use Is_Open , if the file have been create i  want to put some text + the value of Is_Open(should be TRUE) .

There is french in the code :

[code]WITH Ada.Text_IO ;  USE Ada.Text_IO ;

PROCEDURE TestFichier IS

   MonFichier : File_type ;
   
BEGIN
   Create( MonFichier,Name => "clone.adb");
   open(MonFichier,In_file,"clone.adb") ;
    if Is_Open(MonFichier) and MonFichier = true
    then put("Le fichier , ouvert ? : ",MonFichier);
    end if;
END TestFichier ;[/code]

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Jacob Sparre Andersen]

comicfanzine@gmail.com writes:

> [code]WITH Ada.Text_IO ;  USE Ada.Text_IO ;
>
> PROCEDURE TestFichier IS
>
>    MonFichier : File_type ;
>    
> BEGIN
>    Create( MonFichier,Name => "clone.adb");
>    open(MonFichier,In_file,"clone.adb") ;
>     if Is_Open(MonFichier) and MonFichier = true

What type has 'MonFichier'?  And what type has 'true'?

Greetings,

Jacob
-- 
"The problem with America is stupidity. I'm not saying there
 should be a capital punishment for stupidity, but why don't
 we just take the safety labels off of everything and let
 the problem solve itself?"

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[AdaMagica]

Am Montag, 26. Oktober 2015 14:28:22 UTC+1 schrieb comicf...@gmail.com:
> WITH Ada.Text_IO ;  USE Ada.Text_IO ;
> 
> PROCEDURE TestFichier IS
> 
>    MonFichier : File_type ;
>    
> BEGIN
>    Create( MonFichier,Name => "clone.adb");
>    open(MonFichier,In_file,"clone.adb") ;

Se RM A.8.2 for a description of Create and Open.

>     if Is_Open(MonFichier) and MonFichier = true
>     then put("Le fichier , ouvert ? : ",MonFichier);
>     end if;
> END TestFichier ;[/code]

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[J-P. Rosen]

Le 26/10/2015 14:28, comicfanzine@gmail.com a écrit :
> There is french in the code :
If you are more comfortable with French, you can post (in French) to
fr.comp.lang.ada

See you there!

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[comicfanzine]

Le lundi 26 octobre 2015 12:27:53 UTC+1, Simon Wright a écrit :
> comicfanzine@gmail.com writes:
> 
> > Can someone please show my a code in which this function is used , i'm
> > lost , thanks .
> 
> You could try googling <ada text_io is_open>; finds
> http://homepage.ntlworld.com/phil.brooke/topal/hg/topal/misc.adb as the
> 5th or 6th hit.
> 
> Or you could help us to help you by showing us how far you've got
> already; "i'm lost" isn't informative.

Thanks everybody , here is the code with corrections , please read the end :

[code]WITH Ada.Text_IO ;  USE Ada.Text_IO ; 

PROCEDURE TestFichier IS

   MonFichier : File_type ; 
   
BEGIN 
   Create( MonFichier,Name => "clone.adb");
  if Is_Open (MonFichier) then
   Put (Item => "Le fichier , ouvert ? : ", File => MonFichier);
end if;
END TestFichier ;[/code]The code compile but you don't understand what i want to do . I want to create a file (the use of the create procedure will erase+remplace it if he already exist ) , then use IS_open to have a output in comand that say(fonction put) for exemple : "the file have been opened successfuly , value : true " (i repeate,; by put the Value of IS_open : should be true .)

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Simon Wright]

comicfanzine@gmail.com writes:

> The code compile but you don't understand what i want to do . I want
> to create a file (the use of the create procedure will erase+remplace
> it if he already exist ) , then use IS_open to have a output in comand
> that say(fonction put) for exemple : "the file have been opened
> successfuly , value : true " (i repeate,; by put the Value of IS_open
> : should be true .)

You could write

    put(File => MonFichier,
        Item => "Le fichier , ouvert ? : "
                & Boolean'Image (Is_Open (MonFichier)));

(note, if you use named parameter association the order of parameters
doesn't matter).

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[comicfanzine]

Le mardi 27 octobre 2015 12:34:50 UTC+1, Simon Wright a écrit :
> comicfanzine@gmail.com writes:
> 
> > The code compile but you don't understand what i want to do . I want
> > to create a file (the use of the create procedure will erase+remplace
> > it if he already exist ) , then use IS_open to have a output in comand
> > that say(fonction put) for exemple : "the file have been opened
> > successfuly , value : true " (i repeate,; by put the Value of IS_open
> > : should be true .)
> 
> You could write
> 
>     put(File => MonFichier,
>         Item => "Le fichier , ouvert ? : "
>                 & Boolean'Image (Is_Open (MonFichier)));
> 
> (note, if you use named parameter association the order of parameters
> doesn't matter).

Thanks that wanted to do . If i could i put [Solved] on the title on this suject .

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[comicfanzine]

Le lundi 26 octobre 2015 12:27:53 UTC+1, Simon Wright a écrit :
> comicfanzine@gmail.com writes:
> 
> > Can someone please show my a code in which this function is used , i'm
> > lost , thanks .
> 
> You could try googling <ada text_io is_open>; finds
> http://homepage.ntlworld.com/phil.brooke/topal/hg/topal/misc.adb as the
> 5th or 6th hit.
> 
> Or you could help us to help you by showing us how far you've got
> already; "i'm lost" isn't informative.

Thanks everybody , here is the code with corrections :

[code]WITH Ada.Text_IO ;  USE Ada.Text_IO ; 

PROCEDURE TestFichier IS

   MonFichier : File_type ; 
   
BEGIN 
   Create( MonFichier,Name => "clone.adb");
  if Is_Open (MonFichier) then
   Put (Item => "Le fichier , ouvert ? : ", File => MonFichier);
end if;
END TestFichier ;[/code]
The code compile but you don't understand what i wan t to do . I want to create a file (the use of the create procedure will erase+remplace it if he already exist ) , then use IS_open to have a output in comand that say(fonction put) for exemple : "the file have been opened successfuly , value : true " (i repeate , i want to put the Value of IS_open : should be true ).

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Jeffrey R. Carter]

I've reformatted your code to my coding standards.

with Ada.Text_IO;

use Ada.Text_IO;

procedure Testfichier is
   Monfichier : File_Type;
begin
   Create (Monfichier, Name => "clone.adb");

-- If Create succeeds, then Monfichier is open and you get to the "if". If
-- Create fails, it raises an exception and your program ends.

   if Is_Open (Monfichier) then

-- If you get to this line, then Create succeeded and Monfichier if open, so
-- this test is redundant; Is_Open will always return True.

      Put (Item => "Le fichier , ouvert ? : ", File => Monfichier);
   end if;

-- You probably want to close the file before you end.

end Testfichier;

So your code is functionally equivalent to

with Ada.Text_IO;

use Ada.Text_IO;

procedure Testfichier is
   Monfichier : File_Type;
begin
   Create (Monfichier, Name => "clone.adb");
   Put (Item => "Le fichier , ouvert ? : ", File => Monfichier);
end Testfichier;

Since you want it to output the result of Is_Open, and we know that will always
be True, and we should close the file, I'd end up with

with Ada.Text_IO;

procedure Testfichier is
   Monfichier : Ada.Text_IO.File_Type;
begin
   Ada.Text_IO.Create (File => Monfichier, Name => "clone.adb");
   Ada.Text_IO.Put_Line
      (Item => "Le fichier , ouvert ? : True", File => Monfichier);
   Ada.Text_IO.Close (File => Monfichier);
end Testfichier;

-- 
Jeff Carter
"You cheesy lot of second-hand electric donkey-bottom biters."
Monty Python & the Holy Grail
14

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Bob Duff]

comicfanzine@gmail.com writes:

> Can someone please show my a code in which this function is used , i'm
> lost , thanks .

Most code is written so that it is statically known whether a file is
open, so Is_Open is close to useless.  Not entirely useless -- you might
use it in an assertion, such as:

    subtype Open_File is File with Predicate => Is_Open(Open_File);

And Niklas Holsti gave a fairly realistic example where it is NOT
statically known whether the file is open, so the program checks at run
time.

- Bob

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Mon, 26 Oct 2015 18:48:51 -0400, Bob Duff wrote:

> comicfanzine@gmail.com writes:
> 
>> Can someone please show my a code in which this function is used , i'm
>> lost , thanks .
> 
> Most code is written so that it is statically known whether a file is
> open, so Is_Open is close to useless.  Not entirely useless -- you might
> use it in an assertion, such as:
> 
>     subtype Open_File is File with Predicate => Is_Open(Open_File);

In order to have the Constraint_Error exception instead of Status_Error?
Looks entirely useless to me.

> And Niklas Holsti gave a fairly realistic example where it is NOT
> statically known whether the file is open, so the program checks at run
> time.

Yes, but you cannot put a constraint on an existing object. Thus Niklas
example does not apply. 

[ Dynamic predicates never make any sense. ]

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Bob Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Mon, 26 Oct 2015 18:48:51 -0400, Bob Duff wrote:
>
>> comicfanzine@gmail.com writes:
>> 
>>> Can someone please show my a code in which this function is used , i'm
>>> lost , thanks .
>> 
>> Most code is written so that it is statically known whether a file is
>> open, so Is_Open is close to useless.  Not entirely useless -- you might
>> use it in an assertion, such as:
>> 
>>     subtype Open_File is File with Predicate => Is_Open(Open_File);
>
> In order to have the Constraint_Error exception instead of Status_Error?

No, in order to document the fact that a certain formal parameter must
be open, and in order to prove things statically.  If a procedure takes
"F: Open_File", then we can easily prove that writes to F within that
procedure do not raise Status_Error.

> Looks entirely useless to me.

- Bob

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[G.B.]

On 27.10.15 14:30, Bob Duff wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

>>> Most code is written so that it is statically known whether a file is
>>> open, so Is_Open is close to useless.  Not entirely useless -- you might
>>> use it in an assertion, such as:
>>>
>>>      subtype Open_File is File with Predicate => Is_Open(Open_File);
>>
>> In order to have the Constraint_Error exception instead of Status_Error?
>
> No, in order to document the fact that a certain formal parameter must
> be open, and in order to prove things statically.  If a procedure takes
> "F: Open_File", then we can easily prove that writes to F within that
> procedure do not raise Status_Error.
>
>> Looks entirely useless to me.
>
> - Bob

A big Thank You for providing a example of the usefulness of predicates!

The part that refers to formally "documenting" what is expected,
be it expressible in the static type system or not, deserves more
attention IMHO. (Not every project has the time and money
for fully analyzing and transforming programs until the compiler
is capable of tackling everything before run-time. Does anyone
expect all possible and reasonable Boolean expressions to be
statically computable in the near future? Are they therefore
useless?)

Meyer has recently communicated that understanding classes means
to know the classes' contracts. This reminded me of a similar
effect ascribed to unit tests.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Tue, 27 Oct 2015 09:30:54 -0400, Bob Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Mon, 26 Oct 2015 18:48:51 -0400, Bob Duff wrote:
>>
>>> comicfanzine@gmail.com writes:
>>> 
>>>> Can someone please show my a code in which this function is used , i'm
>>>> lost , thanks .
>>> 
>>> Most code is written so that it is statically known whether a file is
>>> open, so Is_Open is close to useless.  Not entirely useless -- you might
>>> use it in an assertion, such as:
>>> 
>>>     subtype Open_File is File with Predicate => Is_Open(Open_File);
>>
>> In order to have the Constraint_Error exception instead of Status_Error?
> 
> No, in order to document the fact that a certain formal parameter must
> be open, and in order to prove things statically.  If a procedure takes
> "F: Open_File", then we can easily prove that writes to F within that
> procedure do not raise Status_Error.

That does not make sense either. There is nothing in the procedure itself 
that would prevent raising Status_Error. Everything is on the caller's 
side. How do you know if some callers would not appreciate Status_Error as 
a possible outcome? Looks like poor design to me.

Anyway proving either of the conditions A) not raising Constraint_Error, B) 
not raising Status_Error look equally hard.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[G.B.]

On 27.10.15 16:26, Dmitry A. Kazakov wrote:
> How do you know if some callers would not appreciate Status_Error as
> a possible outcome?

Actually, this situation is what contracts are made for,
I think:
as a caller, you say what you want the procedure to do,
or else you don't sign this contract. I.e., a redesign
via ECR is in order before you sign.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Tue, 27 Oct 2015 17:43:36 +0100, G.B. wrote:

> On 27.10.15 16:26, Dmitry A. Kazakov wrote:
>> How do you know if some callers would not appreciate Status_Error as
>> a possible outcome?
> 
> Actually, this situation is what contracts are made for,
> I think:
> as a caller, you say what you want the procedure to do,
> or else you don't sign this contract. I.e., a redesign
> via ECR is in order before you sign.

Sure, except that you don't subscribe the contract you cannot fulfill.

The point can be summarized this way. If an exception is a part of the
contract then Status_Error is much better than Constraint_Error and is
already there. If the contract is not to raise, then, firstly, there is no
way to enforce it, and, secondly, if there were a way, proving no
Status_Error would be no harder than no Constraint_Error. Ergo, no use.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Georg Bauhaus]

On 27.10.15 21:04, Dmitry A. Kazakov wrote:
> On Tue, 27 Oct 2015 17:43:36 +0100, G.B. wrote:
>
>> On 27.10.15 16:26, Dmitry A. Kazakov wrote:
>>> How do you know if some callers would not appreciate Status_Error as
>>> a possible outcome?
>>
>> Actually, this situation is what contracts are made for,
>> I think:
>> as a caller, you say what you want the procedure to do,
>> or else you don't sign this contract. I.e., a redesign
>> via ECR is in order before you sign.
>
> Sure, except that you don't subscribe the contract you cannot fulfill.

Yes, an impasse is a possible situation when negotiating contracts.
The interests of the business people will give way to at least
one resolution.

> The point can be summarized this way. If an exception is a part of the
> contract then Status_Error is much better than Constraint_Error

"Better than Assertion_Error?" I understand we are going to get

    subtype Open_File is File with Predicate =>
       Is_Open(Open_File) or else raise Status_Error with "...";

If the Predicate is associated with a subtype, the "specializing"
message after WITH cannot very special. It can be more special when
associated with a subprogram, though. But it can be special in
any case.
  
> If the contract is not to raise, then, firstly, there is no
> way to enforce it,

Enforcing it appears possible in the above case, at least for each
single program involving file objects, IIUC.

> and, secondly, if there were a way, proving no
> Status_Error would be no harder than no Constraint_Error. Ergo, no use.
  
Whenever one defines "use" to have the same meaning as "proof",
then the argument is an elaborate tautology. Now that will be an almost
useless definition 8-)

However, another use of predicates is to document assumptions.
If the assumptions are correct, but the compiler cannot determine
their truth, should we hide the assumptions?

Is it possible to redesign the subtypes etc below, making them
private types instead, so that the compiler "knows" all objects
to have the desired properties? What's the impact on O(?)?

package Conj is

    --
    --  dumb tests; we actually know all the numbers, the point is
    --  to be able to refer to them in assumptions, for the contract.
    --

    subtype Candidate is Positive range 2 .. Positive'Last;

    function Is_Prime (N : Candidate) return Boolean
      is (not (for Some X in 2 .. Candidate'Pred(N) => N rem X = 0));

    subtype Known_Range is Natural
      range 0 .. Natural'Min (Natural'Last, 4 * 10**17);

    subtype GN is Known_Range with Predicate =>   --  dynamic
      (if
         GN >= 4 and GN rem 2 = 0
       then (for Some A in 2 .. GN =>
               (for Some B in 2 .. GN =>
                  Is_Prime (A) and Is_Prime (B)
                  and GN = A + B)));

end Conj;

Running an unnecessary test may burn a CPU core,

with Conj;
procedure Test_Conj
is
    Test : constant Conj.GN := 1234567890;
begin
    null;
end Test_Conj;

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Randy Brukardt]

"Georg Bauhaus" <bauhaus@futureapps.invalid> wrote in message 
news:n0qa3q$th8$1@dont-email.me...
...
> "Better than Assertion_Error?" I understand we are going to get
>
>    subtype Open_File is File with Predicate =>
>       Is_Open(Open_File) or else raise Status_Error with "...";

You need to use the aspect Predicate_Failure here, as opposed to raising an 
exception in the predicate expression. (That's different than in a 
precondition.) In this case (and replacing the Gnat-only "predicate" 
aspect):

    subtype Open_File is File with Dynamic_Predicate =>
       Is_Open(Open_File), Predicate_Failure => raise Status_Error with 
"...";

 Else bad things might happen to membership tests:

    if My_File in Open_File then
        Call_Subprogram_That_Requires_an_Open_File (My_File);
    end if;

If My_File is not open, this membership and your subtype would raise 
Status_Error, not False. (This was a tough nut to crack for the ARG. And 
GNAT only recently implemented Predicate_Failure, so with older GNATs you 
have to leave the exception alone.)

                                            Randy.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Wed, 28 Oct 2015 12:06:33 +0100, Georg Bauhaus wrote:

> On 27.10.15 21:04, Dmitry A. Kazakov wrote:

>> The point can be summarized this way. If an exception is a part of the
>> contract then Status_Error is much better than Constraint_Error
> 
> "Better than Assertion_Error?" I understand we are going to get
> 
>     subtype Open_File is File with Predicate =>
>        Is_Open(Open_File) or else raise Status_Error with "...";

Fine, but it is already this way. Operations of Text_IO propagate
Status_Error when the file was not opened. There is no need to check that
twice and that is no "assertion," anyway.

>> If the contract is not to raise, then, firstly, there is no
>> way to enforce it,
> 
> Enforcing it appears possible in the above case, at least for each
> single program involving file objects, IIUC.

How are you going to get a constrained object? File_Type is limited.

[ It is mere wrong design. If you wanted file objects that refer to only
open files, that is no constraint, but a property ensured upon object
creation. ]

>> and, secondly, if there were a way, proving no
>> Status_Error would be no harder than no Constraint_Error. Ergo, no use.
>   
> Whenever one defines "use" to have the same meaning as "proof",

"Use" in this context has the meaning "added value."

> However, another use of predicates is to document assumptions.

Documenting *shall* have *no* run-time effects.

> If the assumptions are correct, but the compiler cannot determine
> their truth, should we hide the assumptions?

As hide from the compiler? Certainly so! If as you said the compiler has no
idea what your assumption is supposed to mean, how can it generate a useful
code? If you force it, it generates garbage, which the semantics of dynamic
predicates is, a garbage.
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Bob Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Wed, 28 Oct 2015 12:06:33 +0100, Georg Bauhaus wrote:
>> However, another use of predicates is to document assumptions.
>
> Documenting *shall* have *no* run-time effects.

Really?!

In C, we can write:

    int num_gizmos = 0; // num_gizmos is always between 0 and 1024.

In Ada, we can write:

    type Gizmo_Count is range 0 .. 2**10;
    Num_Gizmos: Gizmo_Count := 0;

IMHO, documenting the 0..1024 requirement in executable code is much
better than using a comment:

    - It's more likely to be correct, especially if we have a good test
      suite.  The comment just says what the original programmer thought
      was true.  Maybe they were wrong.  More likely, they were right,
      but subsequent changes elsewhere made the comment wrong.

    - If I'm debugging a specific bug, and the run-time checks on
      Num_Gizmos don't fail, I know the problem isn't caused by an
      out-of-bounds value of that variable.  Even if the
      "range 0..2**10" is wrong, it's not the cause of THIS bug.

    - English comments can be ambiguous -- sometimes "between" means
      inclusive of the end points, sometimes exclusive (although we can
      guess "inclusive" in this case).  On the other hand, I know
      exactly what ".." means.

By the way, what exactly do you mean by "shall"?  A native speaker of
English doesn't usually use that word, except in legal documents and the
like.  You seem to use the word "shall" to express opinions about the
way things ought to be, which seems like an odd usage to me.

- Bob

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Wed, 28 Oct 2015 16:36:09 -0400, Bob Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Wed, 28 Oct 2015 12:06:33 +0100, Georg Bauhaus wrote:
>>> However, another use of predicates is to document assumptions.
>>
>> Documenting *shall* have *no* run-time effects.
> 
> Really?!
> 
> In C, we can write:
> 
>     int num_gizmos = 0; // num_gizmos is always between 0 and 1024.
> 
> In Ada, we can write:
> 
>     type Gizmo_Count is range 0 .. 2**10;
>     Num_Gizmos: Gizmo_Count := 0;
> 
> IMHO, documenting the 0..1024 requirement in executable code is much
> better than using a comment:

How is that documenting? It is a direct instruction to the compiler.
Documentation is addressed to the human reader.

The advantage of Ada over C is that where in Ada you can instruct, in C the
only way is to document.

> By the way, what exactly do you mean by "shall"?  A native speaker of
> English doesn't usually use that word, except in legal documents and the
> like.  You seem to use the word "shall" to express opinions about the
> way things ought to be, which seems like an odd usage to me.

OK

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[AdaMagica]

Am Mittwoch, 28. Oktober 2015 22:02:17 UTC+1 schrieb Dmitry A. Kazakov:
> > In Ada, we can write:
> > 
> >     type Gizmo_Count is range 0 .. 2**10;
> >     Num_Gizmos: Gizmo_Count := 0;
> > 
> > IMHO, documenting the 0..1024 requirement in executable code is much
> > better than using a comment:
> 
> How is that documenting? It is a direct instruction to the compiler.
> Documentation is addressed to the human reader.
> 
> The advantage of Ada over C is that where in Ada you can instruct, in C the
> only way is to document.

IMHO, this is again a case of Dmitry's special nomenclature:
Documentation is not what is evaluable by the compiler; documentation is in comments or in separate documents (like design docs).

I think the Ada community has a different bias: Expressing requirements, i.e. documentation, in code is preferable. Thus we use Natural rather than Integer  for counting, use constraints like above in Gizmo. And we call this *documenting*. This is both, an instruction for the compiler *and* information addressed to the reader.

My two EURO cents.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Thu, 29 Oct 2015 04:25:06 -0700 (PDT), AdaMagica wrote:

> Am Mittwoch, 28. Oktober 2015 22:02:17 UTC+1 schrieb Dmitry A. Kazakov:
>>> In Ada, we can write:
>>> 
>>>     type Gizmo_Count is range 0 .. 2**10;
>>>     Num_Gizmos: Gizmo_Count := 0;
>>> 
>>> IMHO, documenting the 0..1024 requirement in executable code is much
>>> better than using a comment:
>> 
>> How is that documenting? It is a direct instruction to the compiler.
>> Documentation is addressed to the human reader.
>> 
>> The advantage of Ada over C is that where in Ada you can instruct, in C the
>> only way is to document.
> 
> IMHO, this is again a case of Dmitry's special nomenclature:

It is the standard meaning of the word: to record something in written,
graphic or other form; to support or accompany with documentation.

> I think the Ada community has a different bias: Expressing requirements,
> i.e. documentation, in code is preferable.

Actually there are people in c.l.a. against excessive commenting.

> Thus we use Natural rather than
> Integer  for counting, use constraints like above in Gizmo. And we call
> this *documenting*. This is both, an instruction for the compiler *and*
> information addressed to the reader.

So, according to you

   X : Integer;  -- Undocumented
   Y : Natural; -- Documented

Don't you find it a bit silly? There is no difference between both.

BTW, any numeric type in Ada is constrained => "documented", according to
you.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[AdaMagica]

Am Donnerstag, 29. Oktober 2015 14:37:47 UTC+1 schrieb Dmitry A. Kazakov:
> Actually there are people in c.l.a. against excessive commenting.

What is *excessive* commenting?
There is no self-documenting code, nowhere.

> So, according to you
> 
>    X : Integer;  -- Undocumented
>    Y : Natural; -- Documented
> 
> Don't you find it a bit silly? There is no difference between both.

No difference?

No, I don't find this silly. Both document (which word would you use?) a choice, in a way.

Integer: I need positive and negative numbers; I don't care about the range.
Natural: Negative numbers are not allowed.

type T is range -42 .. +42;  -- no difference to Integer according to you?

This does not save me from documenting the code in separate design documents.

> BTW, any numeric type in Ada is constrained => "documented", according to
> you.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[AdaMagica]

> > Actually there are people in c.l.a. against excessive commenting.
> 
> What is *excessive* commenting?
> There is no self-documenting code, nowhere.

I would even say, most of the programs in the world are insufficiently commented.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Thu, 29 Oct 2015 10:57:15 -0700 (PDT), AdaMagica wrote:

> Am Donnerstag, 29. Oktober 2015 14:37:47 UTC+1 schrieb Dmitry A. Kazakov:
>> Actually there are people in c.l.a. against excessive commenting.
> 
> What is *excessive* commenting?
> There is no self-documenting code, nowhere.

What about this:

   if X > 0 then -- When X is positive
      ...
   else -- When X is zero or negative
      ...
   end if;

>> So, according to you
>> 
>>    X : Integer;  -- Undocumented
>>    Y : Natural; -- Documented
>> 
>> Don't you find it a bit silly? There is no difference between both.
> 
> No difference?
> 
> No, I don't find this silly. Both document (which word would you use?) a choice, in a way.

So, what does not document, then?

> Integer: I need positive and negative numbers; I don't care about the range.
> Natural: Negative numbers are not allowed.
> 
> type T is range -42 .. +42;  -- no difference to Integer according to you?

Regarding documentation? None. Neither document anything. They declare
types and objects of certain properties, that is.

A documentation would refer to the problem space and point out other things
that cannot be expressed in the language.

My point was that comparing to C's rough equivalent

   typedef T int;

in Ada less documentation would be required, because the language can
express more, in particular, the values range, the behavior when the range
is violated etc.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Jacob Sparre Andersen]

AdaMagica <christ-usch.grein@t-online.de> writes:

> What is *excessive* commenting?

All comments are in my view excessive. - That doesn't mean that they
aren't occasionally necessary, but the ideal must in my view be that
what we pass to the compiler is also what we ask the programmer to read.

If I have to put comments in my sources I see it as me not being a good
enough programmer to express what I want to do in a way my colleagues
understand.

I'm not against documentation, but I really don't like in-source
comments.

The kind of comments which make sense to me are those which contain a
reference to a detailed explanation of why something is done the way it
is.  I.e. a reference to a mathematical statement, a paper describing an
algorithm or a performance analysis of two competing algorithms.

Greetings,

Jacob
-- 
Why is it that all of the instruments seeking intelligent
life in the universe are pointed away from Earth?

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[J-P. Rosen]

Le 30/10/2015 09:27, Jacob Sparre Andersen a écrit :
> The kind of comments which make sense to me are those which contain a
> reference to a detailed explanation of why something is done the way it
> is.  I.e. a reference to a mathematical statement, a paper describing an
> algorithm or a performance analysis of two competing algorithms.

I agree with you, it is always better to express something in the code
rather than in comments, if possible. But there is a case that cannot be
expressed in code, and must therefore be given as comments: explaining
why you did NOT do something in a certain (and generally more obvious) way.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[G.B.]

On 28.10.15 19:20, Dmitry A. Kazakov wrote:
>> >If the assumptions are correct, but the compiler cannot determine
>> >their truth, should we hide the assumptions?
> As hide from the compiler? Certainly so! If as you said the compiler has no
> idea what your assumption is supposed to mean, how can it generate a useful
> code?

You mean, contract code needs to add value to *executables*
other than run-time tests?

I think the biggest misunderstanding here is in asking for
contracts to be considered just expressions, and then analyzing
them like they were *meant* to be ordinary expressions.

Even so, I think that an implementation of Ada could "outsource"
assertion checking to some read-only copy of the program that
is running on a twin processor, suitably connected, so as to
reduce run-time effects of assertion checking.

> If you force it, it generates garbage, which the semantics of dynamic
> predicates is, a garbage.

No, the compiler will be effecting the computation of a result
that does not need to be computed because we know it is true.
However, we wish to say that we know what the compiler does not
know, because a conjecture is being used as an assumption
when designing our subprogram, say.  If this assertion might
be checked at run-time due to some Assertion_Policy, then we
have to add a contraption,

     Some_Assertion =>
         Conjecture_X_To_Be_Assumed or else Conjecture_X (...);

So, if an algorithm is based on a conjecture, and we wish
to communicate what it is, precisely, a Boolean expression
allows us to do so. It documents our assumptions precisely.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[J-P. Rosen]

Le 29/10/2015 12:47, G.B. a écrit :
> Even so, I think that an implementation of Ada could "outsource"
> assertion checking to some read-only copy of the program that
> is running on a twin processor, suitably connected, so as to
> reduce run-time effects of assertion checking.

IIRC, the old Rational R-1000 did that for constraints: there was a
constraint-checking co-processor running in parallel with the main CPU
(and raising C_E in the main CPU when appropriate).

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Thu, 29 Oct 2015 12:47:48 +0100, G.B. wrote:

> On 28.10.15 19:20, Dmitry A. Kazakov wrote:
>>> >If the assumptions are correct, but the compiler cannot determine
>>> >their truth, should we hide the assumptions?
>> As hide from the compiler? Certainly so! If as you said the compiler has no
>> idea what your assumption is supposed to mean, how can it generate a useful
>> code?
> 
> You mean, contract code needs to add value to *executables*
> other than run-time tests?

I mean that something unknown is, well, unknown.

> I think the biggest misunderstanding here is in asking for
> contracts to be considered just expressions, and then analyzing
> them like they were *meant* to be ordinary expressions.

Yes. Contracts may have no effect on program execution. Consider this:

program describes execution
contract describes program(s)
documentation describes anything

> Even so, I think that an implementation of Ada could "outsource"
> assertion checking to some read-only copy of the program that
> is running on a twin processor, suitably connected, so as to
> reduce run-time effects of assertion checking.

We discussed that earlier. You can have program A asserting program B. You
never can do this in a single program. That is inconsistent.

Any execution effects of A are not of B. Thus, as before, assertion has no
run-time effect on B. Nothing changed.

When you put A into B, that is automatically broken.

>> If you force it, it generates garbage, which the semantics of dynamic
>> predicates is, a garbage.
> 
> No, the compiler will be effecting the computation of a result
> that does not need to be computed because we know it is true.

Either the program raises exception or it does not.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Georg Bauhaus]

On 29.10.15 15:00, Dmitry A. Kazakov wrote:

> Contracts may have no effect on program execution.

(Must have no effect?)

Did I miss why? I saw picking a universe that suffers from failure
to respond usefully to some runs of programs failing, even in some
expected way. There was also the assumption of the existence of a
single allowed run-time effect for each pair <source program, input>.

Naturally, contracts will have no effect at run-time when tools and
brains are capable of demonstrating that all assertions will always
be true. For me, this is just a dream.

>  Consider this:
>
> program describes execution
> contract describes program(s)
> documentation describes anything

Yes, the definitions look like the rattling machinery of clean room
program analysis and fully informed decision making.

HOMER: (stands up) "Boring!"

I think the third line (documentation describing *anything*) is troublesome,
in part because the generality might lead to a paradox, and because it
remains unclear to me if documentation describes program(s) or execution.
Also how, if not using either the contract or the program.

>> Even so, I think that an implementation of Ada could "outsource"
>> assertion checking to some read-only copy of the program that
>> is running on a twin processor, suitably connected, so as to
>> reduce run-time effects of assertion checking.
>
> We discussed that earlier. You can have program A asserting program B. You
> never can do this in a single program. That is inconsistent.

There is no program A, as A is a template. Instances (for runs) are
created when choosing an Assertion_Policy, or levels of optimization,
say. If levels of optimization may change formal semantics (11.6 IIUC),
then why is optimization o.K., but controlling assertion checking is not?
Just because of some thin, formal, logical concern that contracts pushing
us into the morass of recursion is as problematical as most programming?

Anyway, if a Rational R-1000 did perform checks on a coprocessor,
perhaps we just need another word? So that we could say
"formal description of program(s)" when we mean it and use "contract"
instead for what seems to be its "other" meaning?

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Fri, 30 Oct 2015 02:06:43 +0100, Georg Bauhaus wrote:

> On 29.10.15 15:00, Dmitry A. Kazakov wrote:
> 
>> Contracts may have no effect on program execution.
> 
> (Must have no effect?)
> 
> Did I miss why?

Because contracts describe programs.

> I saw picking a universe that suffers from failure
> to respond usefully to some runs of programs failing, even in some
> expected way.

Yes, and the salary is far too low, did I even mention weather? Horrible!

> Naturally, contracts will have no effect at run-time when tools and
> brains are capable of demonstrating that all assertions will always
> be true. For me, this is just a dream.

Only because you call contracts things which are not. Naming is no problem,
which is that any usefulness of contracts is based on clear distinction to
the program itself. Once you confuse them you have no contracts, just
poorly designed implementations. Poorly because considering them
non-behavior, you don't pay attention to what they cause (and they surely
do) at run-time. It is just a lazy self-indulgent way of design, not much
different from C's approach.

>>  Consider this:
>>
>> program describes execution
>> contract describes program(s)
>> documentation describes anything
> 
> Yes, the definitions look like the rattling machinery of clean room
> program analysis and fully informed decision making.
> 
> HOMER: (stands up) "Boring!"

Universe is an extremely boring place, if you look at it.

> I think the third line (documentation describing *anything*) is troublesome,
> in part because the generality might lead to a paradox, and because it
> remains unclear to me if documentation describes program(s) or execution.

It does not because documentation is informal. Things you can describe
formal, you do. The rest goes into documentation.

> Also how, if not using either the contract or the program.

As an old saying say: if nothing else helps read the documentation.

>>> Even so, I think that an implementation of Ada could "outsource"
>>> assertion checking to some read-only copy of the program that
>>> is running on a twin processor, suitably connected, so as to
>>> reduce run-time effects of assertion checking.
>>
>> We discussed that earlier. You can have program A asserting program B. You
>> never can do this in a single program. That is inconsistent.
> 
> There is no program A, as A is a template. Instances (for runs) are
> created when choosing an Assertion_Policy, or levels of optimization,
> say. If levels of optimization may change formal semantics (11.6 IIUC),
> then why is optimization o.K., but controlling assertion checking is not?
> Just because of some thin, formal, logical concern that contracts pushing
> us into the morass of recursion is as problematical as most programming?

The concern is safe design. If B has bugs it cannot be relied on to
determine if it has them.

> Anyway, if a Rational R-1000 did perform checks on a coprocessor,

Checks are not necessarily correctness checks. There is nothing incorrect
in subscript error or zero divide without further assumptions about the
problem space array or number is used to model.

> perhaps we just need another word? So that we could say
> "formal description of program(s)"

"formal description of program" is the program itself. A programming
language is a formal one. A sentence in this language is a description of a
program (meaning: set of actions) to execute.

> when we mean it and use "contract"
> instead for what seems to be its "other" meaning?

"contract" is a formal description of a *set* of programs or their parts.
It specifies desired properties of shared by all these programs, the
properties other programs can rely on. E.g. Dynamic Is_Open predicate is
not a contract, because you cannot rely on it. It is just a part of the
program itself, misplaced in the declarative region.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[G.B.]

On 30.10.15 09:39, Dmitry A. Kazakov wrote:
> The concern is safe design. If [program] B has bugs it cannot be
 > relied on to determine if it has them.

Uhm, so what?  Which kind of program is relied upon to determine
if it has bugs or not? Would that be a bug free self-debugging
program?

OTOH, what if we can learn about potential bugs because we happen
to think that a failed expression has exactly that potential
for us? Detecting a false positive needs to be assessed empirically.
TTBOMK, assertions failed have so far lead to improvement of
programs.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Fri, 30 Oct 2015 15:32:16 +0100, G.B. wrote:

> On 30.10.15 09:39, Dmitry A. Kazakov wrote:
>> The concern is safe design. If [program] B has bugs it cannot be
>> relied on to determine if it has them.
> 
> Uhm, so what?  Which kind of program is relied upon to determine
> if it has bugs or not?

A program that contains run-time checks for bugs.

> OTOH, what if we can learn about potential bugs because we happen
> to think that a failed expression has exactly that potential
> for us?

What kinds of answer do you expect?

> Detecting a false positive needs to be assessed empirically.

Positive of *what*? You first need a workable definition of a correct
program, which you don't have and cannot have because of the reasons
explained earlier.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[G.B.]

On 30.10.15 17:20, Dmitry A. Kazakov wrote:
> On Fri, 30 Oct 2015 15:32:16 +0100, G.B. wrote:
>
>> On 30.10.15 09:39, Dmitry A. Kazakov wrote:
>>> The concern is safe design. If [program] B has bugs it cannot be
>>> relied on to determine if it has them.
>>
>> Uhm, so what?  Which kind of program is relied upon to determine
>> if it has bugs or not?
>
> A program that contains run-time checks for bugs.

I don't think anybody says that, nor does "contract based design",
not the part with "relying"! As is apparent from the Ada Rationale
("for debugging..."). As was apparent from some quoted paragraphs.

Also of interest is Hoare's idea of a SIMPLYFYING_ASSUMTION.
Which is to be used in some situations(!), but not in others.

>> OTOH, what if we can learn about potential bugs because we happen
>> to think that a failed expression has exactly that potential
>> for us?
>
> What kinds of answer do you expect?

If someone is assuming that programmers will always start their
thinking from something comprehensively correct, I expect his
answer to reflect this.
In other cases, the ones I consider more ordinary, decent
programming, I'd expect this:

"... needs to be assessed empirically."

> Positive of *what*?

Positive of what we now have learned may (not) be the desired outcome.
In some cases, that's too late. In many cases, we stop before rollout.
We might be stymied.

> You first need a workable (...) definition of a correct
> program

What makes you assume that a specific, formalistic definition of
a correct program is the workable one?

Except per the narrow situation-excluding circularity of
"work" = "operation":
Considering the most successful software companies on this
planet, while they do not profit from selling correct (formally,
somehow) programs(*), they still strive for local correctness.
(A program that was correct for Ariane IV was not correct(?) for
... Again, situations!)

So, I guess, one might poke fun at tests that make test runs
of programs fail because the test was failing, one might start
from world-excluding definitions that of necessity produce
a contradiction, or one might make jokes about programming
efforts that assume that sufficient formalization is possible.
All are justified, IMHO.

__
(*) Since, who would pay for updates?

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Fri, 30 Oct 2015 20:07:18 +0100, G.B. wrote:

> On 30.10.15 17:20, Dmitry A. Kazakov wrote:
>> On Fri, 30 Oct 2015 15:32:16 +0100, G.B. wrote:
>>
>>> On 30.10.15 09:39, Dmitry A. Kazakov wrote:
>>>> The concern is safe design. If [program] B has bugs it cannot be
>>>> relied on to determine if it has them.
>>>
>>> Uhm, so what?  Which kind of program is relied upon to determine
>>> if it has bugs or not?
>>
>> A program that contains run-time checks for bugs.
> 
> I don't think anybody says that, nor does "contract based design",

Anybody but you?

>> Positive of *what*?
> 
> Positive of what we now have learned may (not) be the desired outcome.

Thus:

"Detecting a false positive needs to be assessed empirically."

reads as

"Somebody needs empirically assess misinterpretation of desired outcomes as
undesired outcomes..."

May I suggest, for a start, do not misinterpret anything, then you won't
need to assess that later... (:-))

>> You first need a workable (...) definition of a correct
>> program
> 
> What makes you assume that a specific, formalistic definition of
> a correct program is the workable one?

Easy. Any non-contradictory definition is workable.

> Except per the narrow situation-excluding circularity of
> "work" = "operation":

Workable here = logically consistent.

You seem are under a [false] impression that since ideal circles do not
exist the car wheels can be made square...

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Georg Bauhaus]

On 31.10.15 10:31, Dmitry A. Kazakov wrote:

>>>>  Which kind of program is relied upon to determine
                                ^^^^^^
>>>> if it has bugs or not?
>>>
>>> A program that contains run-time checks for bugs.
>>
>> I don't think anybody says that, nor does "contract based design",

Let me put the essential piece back in, the one that you didn't quote:

   “not the part with "relying"!”

> Thus:
>
> "Detecting a false positive needs to be assessed empirically."
>
> reads as
>
> "Somebody needs empirically assess misinterpretation of desired outcomes as
> undesired outcomes..."

Somebody *will* say "This effect was not intended!", after the fact.

(If you could leave the bits in that make clear how a single correct
interpretation before the fact might not exist (when static properties
of programs (to be) are insufficient as a basis for drafting contracts)
...)

> May I suggest, for a start, do not misinterpret anything, then you won't
> need to assess that later... (:-))

So, how do we make sure that we do not misinterpret anything?

By not saying anything, I guess, if Boolean expressions should
not be asserted unless our favorite PL's compiler can handle them
at compile time. Is that right?

(Again, program A is a template.)

> Any non-contradictory definition [of correct program] is workable.

Why?

(Again, program A is a template, no consistency issues.)

>> Except per the narrow situation-excluding circularity of
>> "work" = "operation":
>
> Workable here = logically consistent.

How did the program in Ariane IV logically rest on inconsistency
within it, then? How did its "contract" fail at compile time?

Static properties of programs do not exhaust the material which is
typically put in contracts. Work is done using unknowns, every day.

Conquering the word "contract" to mean nothing but formal semantics
of programs conveniently removes its usual meaning.

It also removes programming techniques that have been seen
to be useful and efficient.

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[G.B.]

On 30.10.15 09:39, Dmitry A. Kazakov wrote:
> you don't pay attention to what [Boolean expressions of
 > assertions checked] cause (and they surely
> do) at run-time.

On the contrary, paying attention to them is part of why
Assertion_Policy is in the language.

I don't want the compiler to be in the way of design. Therefore,
I accept that not all things expressible formally will be static.
I don't want hide these formal assumptions for the same reasons.
That's self-indulgent, then?

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Fri, 30 Oct 2015 15:40:30 +0100, G.B. wrote:

> On 30.10.15 09:39, Dmitry A. Kazakov wrote:
>> you don't pay attention to what [Boolean expressions of
>  > assertions checked] cause (and they surely
>> do) at run-time.
> 
> On the contrary, paying attention to them is part of why
> Assertion_Policy is in the language.

Yes, a part of whatever, except for what the program does...

> I don't want the compiler to be in the way of design.

Surely C would be the best language for this.

> Therefore,
> I accept that not all things expressible formally will be static.
> I don't want hide these formal assumptions for the same reasons.
> That's self-indulgent, then?

Yes, because you sell it yourself as "contracts," as "ways of design," as
anything supposed to convince you having a better program, without taking
care for what actually goes on at run-time!

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Bob Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> On Tue, 27 Oct 2015 09:30:54 -0400, Bob Duff wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>> 
>>> On Mon, 26 Oct 2015 18:48:51 -0400, Bob Duff wrote:
>>>
>>>> comicfanzine@gmail.com writes:
>>>> 
>>>>> Can someone please show my a code in which this function is used , i'm
>>>>> lost , thanks .
>>>> 
>>>> Most code is written so that it is statically known whether a file is
>>>> open, so Is_Open is close to useless.  Not entirely useless -- you might
>>>> use it in an assertion, such as:
>>>> 
>>>>     subtype Open_File is File with Predicate => Is_Open(Open_File);
>>>
>>> In order to have the Constraint_Error exception instead of Status_Error?
>> 
>> No, in order to document the fact that a certain formal parameter must
>> be open, and in order to prove things statically.  If a procedure takes
>> "F: Open_File", then we can easily prove that writes to F within that
>> procedure do not raise Status_Error.
>
> That does not make sense either. There is nothing in the procedure itself 
> that would prevent raising Status_Error. Everything is on the caller's 
> side. How do you know if some callers would not appreciate Status_Error as 
> a possible outcome? Looks like poor design to me.

I don't understand what you're getting at.  We can, of course, make the
Predicate raise Status_Error if we want.  But the point is to prove
statically that files are open when we want to write to them.  The
example of the log file ("We want to write on the file if and only if it
is open") is unusual.  The far more common case is:  "We want to write
on the file.  No 'if's about it.  Therefore, the file had better be
open."

> Anyway proving either of the conditions A) not raising Constraint_Error, B) 
> not raising Status_Error look equally hard.

I think it is important that proofs be localized.  E.g. proving
something about P should not require examining all call sites
that call P.  Suppose we have:

    procedure P(F: in out Open_File) is
    begin
        ...
        Put(F, ...);
        ...
    end P;

At the call to Put, we can (informally) prove that F is open.
(This requires knowing certain things, such as Is_Open not having
side effects, and nobody is sneakily calling Close in the "..." parts.
To automate such a proof, you'd need some way of expressing such
things -- e.g. globals annotations as supported by SPARK 2014.)

The Predicate is pushing the responsibility of opening the file to the
caller.  That's a good thing, because the caller likely knows:

    procedure Caller(Name: String) is
        F: File_Type;
    begin
        Open(F, Name, ...);
        P(F);

We know at "P(F)" that F is open because we just opened it.
Both of these proofs are local and static.  There's no issue
about Constraint_Error versus Assertion_Failure versus Status_Error,
because we know that no exception is raised.

Without the Predicate (or an equivalent precondition), the proofs
fall apart.

I'd say that's the main point of contracts -- to allow localized
reasoning about programs.

- Bob

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Wed, 28 Oct 2015 16:07:55 -0400, Bob Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Tue, 27 Oct 2015 09:30:54 -0400, Bob Duff wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>>> 
>>>> On Mon, 26 Oct 2015 18:48:51 -0400, Bob Duff wrote:
>>>>
>>>>> comicfanzine@gmail.com writes:
>>>>> 
>>>>>> Can someone please show my a code in which this function is used , i'm
>>>>>> lost , thanks .
>>>>> 
>>>>> Most code is written so that it is statically known whether a file is
>>>>> open, so Is_Open is close to useless.  Not entirely useless -- you might
>>>>> use it in an assertion, such as:
>>>>> 
>>>>>     subtype Open_File is File with Predicate => Is_Open(Open_File);
>>>>
>>>> In order to have the Constraint_Error exception instead of Status_Error?
>>> 
>>> No, in order to document the fact that a certain formal parameter must
>>> be open, and in order to prove things statically.  If a procedure takes
>>> "F: Open_File", then we can easily prove that writes to F within that
>>> procedure do not raise Status_Error.
>>
>> That does not make sense either. There is nothing in the procedure itself 
>> that would prevent raising Status_Error. Everything is on the caller's 
>> side. How do you know if some callers would not appreciate Status_Error as 
>> a possible outcome? Looks like poor design to me.
> 
> I don't understand what you're getting at.  We can, of course, make the
> Predicate raise Status_Error if we want.  But the point is to prove
> statically that files are open when we want to write to them.  The
> example of the log file ("We want to write on the file if and only if it
> is open") is unusual.  The far more common case is:  "We want to write
> on the file.  No 'if's about it.  Therefore, the file had better be
> open."

No doubt about it. That does not help to understand how substituting one
exception for another changes anything. A caller still can pass a closed
file in both cases.

>> Anyway proving either of the conditions A) not raising Constraint_Error, B) 
>> not raising Status_Error look equally hard.
> 
> I think it is important that proofs be localized.  E.g. proving
> something about P should not require examining all call sites
> that call P.  Suppose we have:
> 
>     procedure P(F: in out Open_File) is
>     begin
>         ...
>         Put(F, ...);
>         ...
>     end P;

You cannot prove that P does not raise Constraint_Error, in fact it is the
opposite, it does raise, when F is not open.

You could only prove that *if* F is open then Constraint_Error is not
raised. Likewise you could prove that if F is open then Status_Error is not
raised, as locally as for another one. It is just same.

> At the call to Put, we can (informally) prove that F is open.
> (This requires knowing certain things, such as Is_Open not having
> side effects, and nobody is sneakily calling Close in the "..." parts.
> To automate such a proof, you'd need some way of expressing such
> things -- e.g. globals annotations as supported by SPARK 2014.)
> 
> The Predicate is pushing the responsibility of opening the file to the
> caller.  That's a good thing, because the caller likely knows:
> 
>     procedure Caller(Name: String) is
>         F: File_Type;
>     begin
>         Open(F, Name, ...);
>         P(F);
> 
> We know at "P(F)" that F is open because we just opened it.
> Both of these proofs are local and static.  There's no issue
> about Constraint_Error versus Assertion_Failure versus Status_Error,
> because we know that no exception is raised.
> 
> Without the Predicate (or an equivalent precondition), the proofs
> fall apart.

They don't because Text_IO procedures have contracts not to raise
Status_Error. This is fully equivalent. You cannot say that they don't have
contracts because your proof is necessarily based on these implied
contracts.

> I'd say that's the main point of contracts -- to allow localized
> reasoning about programs.

Yes, and these contracts exist as documented in ARM. The only problem is
that they are not explicit.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[G.B.]

On 27.10.15 09:30, Dmitry A. Kazakov wrote:
> Yes, but you cannot put a constraint on an existing object.

Why would that be important, given objects' states, and also
type conversions?

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[Dmitry A. Kazakov]

On Tue, 27 Oct 2015 15:02:18 +0100, G.B. wrote:

> On 27.10.15 09:30, Dmitry A. Kazakov wrote:
>> Yes, but you cannot put a constraint on an existing object.
> 
> Why would that be important, given objects' states, and also
> type conversions?

That was not my point. The point is that the object is the example at hand
is unconstrained. It is valid and a *use case* for a log file to be closed.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: function Is_Open (File : File_Type) return Boolean; :Text_io

[G.B.]

On 27.10.15 16:10, Dmitry A. Kazakov wrote:
> On Tue, 27 Oct 2015 15:02:18 +0100, G.B. wrote:
>
>> On 27.10.15 09:30, Dmitry A. Kazakov wrote:
>>> Yes, but you cannot put a constraint on an existing object.
>>
>> Why would that be important, given objects' states, and also
>> type conversions?
>
> That was not my point. The point is that the object is the example at hand
> is unconstrained. It is valid and a *use case* for a log file to be closed.

O.K., as I read it, Bob's reply works convincingly if considered rather
self-contained. And with reference to typical logging situations?

(I agree that there are varying expectations regarding a log file,
one implied by the example, viz. writing only if the file is open
and silently "ignoring" the call otherwise. But this seems a rather
far fetched setup to me. I'd expect that a log file that is not in
an open state should raise, degrees of verbosity of logging being
part of configuration. A specific exception pinpoints the error.)