Tests in a software release

Tests in a software release

[Victor Porton]

Do you agree that a release (that is software for which debugging was 
finished) should have integer overflow tests but not array out of bounds 
tests (because array out of bounds is always a programming error, but 
integer overflow may happen in an innocent program)?

-- 
Victor Porton - http://portonvictor.org

Re: Tests in a software release

[Dmitry A. Kazakov]

On 25/10/2017 21:30, Victor Porton wrote:
> Do you agree that a release (that is software for which debugging was
> finished) should have integer overflow tests but not array out of bounds
> tests (because array out of bounds is always a programming error, but
> integer overflow may happen in an innocent program)?

Neither check can be disabled.

1. Both are contracted behavior. Disabling checks breaks the contract 
unless proven otherwise and *statically*. In the latter case it is an 
optimization issue to remove the check when that does not change the 
program behavior.

2. Any error must be detected as early as possible, so better bounds 
check now than a memory corruption check later. Therefore no difference 
if check failure were expected or not.

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

Re: Tests in a software release

[Stefan.Lucks]

[-- Attachment #1: Type: text/plain, Size: 2355 bytes --]

On Wed, 25 Oct 2017, Victor Porton wrote:

> Do you agree that a release (that is software for which debugging was
> finished) should have integer overflow tests but not array out of bounds
> tests (because array out of bounds is always a programming error, but
> integer overflow may happen in an innocent program)?


Firstly, depending on your programming conventions (or style) either 
exception can be an error, or both, or none. As a rule of thumb, if the 
possibility for the exception is anticipated and the exception is handled,
it is not an error. If you don't anticipate the exception to be raised, 
raising it is an error.

Here a simple example for a program where an out-of-bounds access to an 
array is not an error, and skipping the check would break the program:

with Ada.Text_IO;

procedure Example is

    type Counter_Array is array (Character range <>) of Integer;
    Counter: Counter_Array('a' .. 'z') := (others => 0);

begin
    while not Ada.Text_IO.End_Of_File loop
       declare
          C: Character;
       begin
          Ada.Text_IO.Get(C);
          Counter(C) := Counter(C) + 1;
          Ada.Text_IO.Put_Line(C & Integer'Image(Counter(C)));
       exception
          when others => null;
       end;
    end loop;
    for C in Counter'Range loop
       Ada.Text_IO.Put(Integer'Image(Counter(C)));
    end loop;
end Example;


Secondly, even if raising the exception is an error, why do you want to 
skip the check?

Raising the exception gives you at least the chance to shut down your 
program cleanly (try to close files you opened ...) and to write some 
debugging output.

Of course, if it turns out that your program is too slow, skipping either 
check may be an option. Ideally, you only do so after properly profiling 
your program and locally, for the parts of the program which are 
performance bottlenecks. Generally turning of some checks from scratch is 
premature optimization. (BTW, my general experience is that skipping 
overflow and out-of-bounds access checks improves the peformance only 
marginally.)



--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----

Re: Tests in a software release

[Simon Clubley]

On 2017-10-25, Victor Porton <porton@narod.ru> wrote:
> Do you agree that a release (that is software for which debugging was 
> finished) should have integer overflow tests but not array out of bounds 
> tests (because array out of bounds is always a programming error, but 
> integer overflow may happen in an innocent program)?
>

No way should they ever be disabled. You only _think_ that debugging
is finished. :-)

Leave them enabled and have a failsafe handler do whatever is needed
either to shut things down or to recover in a controlled manner.

Simon.

-- 
Simon Clubley, clubley@remove_me.eisner.decus.org-Earth.UFP
Microsoft: Bringing you 1980s technology to a 21st century world

Re: Tests in a software release

[G. B.]

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

> Disabling checks breaks the contract 

Disabling checks means to rely on a contract!
The contract states what you may assume.

It is worrisome when a thing‘s properties are
named its „contract“. They are simply non-
negotiable properties. There is no “between”
like there is between parties of “contract”.

Don’t let consultants redefine ordinary words.

Re: Tests in a software release

[Dmitry A. Kazakov]

On 2017-10-27 20:06, G. B. wrote:
> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
> 
>> Disabling checks breaks the contract
> 
> Disabling checks means to rely on a contract!

No. The contract requires Constraint_Error propagation. Disabling checks 
breaks that.

The intention of allowing checks being disabled was to allow manual 
optimization in very few cases when the preconditions are known to be 
stronger than specified. The source of this knowledge is unknown, it is 
up to the code maintainer to assert it. For this reason disabling checks 
cannot be the rule in contrary to what Victor suggested.

> The contract states what you may assume.

The contract defines partial behavior.

> It is worrisome when a thing‘s properties are
> named its „contract“.

Some properties are contracted some are not. Nothing to worry about...

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

Re: Tests in a software release

[G.B.]

On 27.10.17 20:54, Dmitry A. Kazakov wrote:
> The contract requires Constraint_Error propagation.

Checks require Constraint_Error propagation.

Re: Tests in a software release

[Dmitry A. Kazakov]

On 2017-10-28 08:53, G.B. wrote:
> On 27.10.17 20:54, Dmitry A. Kazakov wrote:
>> The contract requires Constraint_Error propagation.
> 
> Checks require Constraint_Error propagation.

Checks ensure Constraint_Error as a part of implementation.

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

Re: Tests in a software release

[G. B.]

Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
> On 2017-10-28 08:53, G.B. wrote:
>> On 27.10.17 20:54, Dmitry A. Kazakov wrote:
>>> The contract requires Constraint_Error propagation.
>> 
>> Checks require Constraint_Error propagation.
> 
> Checks ensure Constraint_Error as a part of implementation.
> 

Implementation of checks, not of contracts.

Re: Tests in a software release

[Dmitry A. Kazakov]

On 2017-10-30 21:44, G. B. wrote:
> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
>> On 2017-10-28 08:53, G.B. wrote:
>>> On 27.10.17 20:54, Dmitry A. Kazakov wrote:
>>>> The contract requires Constraint_Error propagation.
>>>
>>> Checks require Constraint_Error propagation.
>>
>> Checks ensure Constraint_Error as a part of implementation.
> 
> Implementation of checks, not of contracts.

This is exactly same.

Note that all run-time effect of the syntactic language construct named 
"call of a subroutine X" is the implementation of X.

There is nothing that is not implementation of. There is nothing that is 
not behavior. There is nothing that may not fall under the contract. It 
is irrelevant if and which parts of the implementation are inlined and 
which are re-entrant. It is irrelevant how they are ordered to the 
machine instruction "CALL", "JSB", whatever. It is irrelevant how they 
are associated with the stack frame if any. All this is the implementation.

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

Re: Tests in a software release

[G.B.]

On 30.10.17 21:56, Dmitry A. Kazakov wrote:
> On 2017-10-30 21:44, G. B. wrote:
>> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
>>> On 2017-10-28 08:53, G.B. wrote:
>>>> On 27.10.17 20:54, Dmitry A. Kazakov wrote:
>>>>> The contract requires Constraint_Error propagation.
>>>>
>>>> Checks require Constraint_Error propagation.
>>>
>>> Checks ensure Constraint_Error as a part of implementation.
>>
>> Implementation of checks, not of contracts.
> 
> This is exactly same.

So, Ada programs will check theirs checks?

Expectations can be stated in comments,
or be part of accompanying documentation and still
be part of a contract.

> There is nothing that is not behavior.

Checking is behavior. However, let SPARK check conditions
of a contract, and let the result be Truth. Then they
have been checked before the program even runs, and
turning *off* Ada checks is, therefore, justified.

Disabling Ada checks means to rely on this contract.

> There is nothing that may not fall under the contract.

There are very many things, even in a program,
that do exist, exhibit behavior, but are not
part of any known, non-fictional contract, such as
the transitive closure of an unspeakable hypothesis.

Re: Tests in a software release

[Dmitry A. Kazakov]

On 2017-10-31 08:17, G.B. wrote:
> On 30.10.17 21:56, Dmitry A. Kazakov wrote:
>> On 2017-10-30 21:44, G. B. wrote:
>>> Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:
>>>> On 2017-10-28 08:53, G.B. wrote:
>>>>> On 27.10.17 20:54, Dmitry A. Kazakov wrote:
>>>>>> The contract requires Constraint_Error propagation.
>>>>>
>>>>> Checks require Constraint_Error propagation.
>>>>
>>>> Checks ensure Constraint_Error as a part of implementation.
>>>
>>> Implementation of checks, not of contracts.
>>
>> This is exactly same.
> 
> So, Ada programs will check theirs checks?

Implementation of bounds check = implementation of contract on bounds check.

It is called tautology.

> Expectations can be stated in comments,
> or be part of accompanying documentation and still
> be part of a contract.
> 
>> There is nothing that is not behavior.
> 
> Checking is behavior. However, let SPARK check conditions
> of a contract, and let the result be Truth. Then they
> have been checked before the program even runs, and
> turning *off* Ada checks is, therefore, justified.

That is what I said. Checks can be removed only when statically proven 
not to fail. This is called optimization.

If in the IF-statement the condition is proven statically true, the 
ELSE-part can be removed. Just same.

Ada could have a pragma to remove all ELSE parts of all IF-statements. 
Would anybody argue for that? (:-))

> Disabling Ada checks means to rely on this contract.

It relays on proven properties of the program.

>> There is nothing that may not fall under the contract.
> 
> There are very many things, even in a program,
> that do exist, exhibit behavior, but are not
> part of any known, non-fictional contract, such as
> the transitive closure of an unspeakable hypothesis.

Sure. Contract only limits behavior it does not specify it. The point is 
that any run-time check is behavior of the callee and cannot be argued 
something belonging to the caller or to whatever else. Body may be not 
all behavior, e.g. if the check happens on the caller's side of the call.

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

Re: Tests in a software release

[G.B.]

On 31.10.17 09:32, Dmitry A. Kazakov wrote:

> Implementation of bounds check = implementation of contract on bounds check.

To declare that the different names of different
things shall mean the same is one way of cutting
the Gordian knot.


> Checks can be removed only when statically proven not to fail.

Programmers may remove checks whenever they think
they should. No fancy proof is required(*).

> This is called optimization.

Optimization means that a compiler translates
source text using different algorithms.

Contracts between clients and suppliers do not
need a compiler. They do not require source text.
They need a lawyer. No, I am not joking.

>  The point is that any run-time check is behavior of the callee and cannot be argued something belonging to the caller or to whatever else.

Checks have actually belonged to something else,
on useful hardware, as has been explained in the past.

But your description of typical translations of
Ada programs that carry checks is about today's checks
in GNAT output. It's not even about contracts, which
are a purely legal thing between parties.

__
(*) It has been proven is that programs proven correct
will of necessity be rare or impractical.

Re: Tests in a software release

[Dmitry A. Kazakov]

On 03/11/2017 08:24, G.B. wrote:
> On 31.10.17 09:32, Dmitry A. Kazakov wrote:
> 
>> Checks can be removed only when statically proven not to fail.
> 
> Programmers may remove checks whenever they think
> they should. No fancy proof is required(*).

Yes, as with any bug, the programmer has an undeniable right to 
introduce it.

>> This is called optimization.
> 
> Optimization means that a compiler translates
> source text using different algorithms.

No.

Optimization is varying the implementation within the braces of the 
contract in order to achieve certain goal, e.g. to reduce memory usage.

> Contracts between clients and suppliers do not
> need a compiler.

Removing checks is not related to enforcement of contracts. It is tuning 
the implementation. So long the contract is not violated by that, it is 
all OK. If it gets violation it is a bug. No rocket science here.

>>  The point is that any run-time check is behavior of the callee and 
>> cannot be argued something belonging to the caller or to whatever else.
> 
> Checks have actually belonged to something else,
> on useful hardware, as has been explained in the past.

Has it been explained that some hardware has instruction ADD? Does it 
mean that "+" has no implementation? Whichever way calls to the caller 
are translated is irrelevant. Again, all effect is the implementation. 
There is no anything else.

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

Re: Tests in a software release

[Shark8]

On Friday, November 3, 2017 at 1:24:53 AM UTC-6, G.B. wrote:
> 
> __
> (*) It has been proven is that programs proven correct
> will of necessity be rare or impractical.

Counterproof:
The Ironsides DNS is proven correct, is practical, and was used to test whether formal methods & provers can be used practically to produce non-trivial useful programs. -- http://ironsides.martincarlisle.com/

Re: Tests in a software release

[G.B.]

On 03.11.17 13:49, Shark8 wrote:
> On Friday, November 3, 2017 at 1:24:53 AM UTC-6, G.B. wrote:
>>
>> __
>> (*) It has been proven is that programs proven correct
>> will of necessity be rare or impractical.
> 
> Counterproof:
> The Ironsides DNS is proven correct, is practical, and was used to test whether formal methods & provers can be used practically to produce non-trivial useful programs. -- http://ironsides.martincarlisle.com/

How is "practical" the opposite of "rare or impractical"?

This was a rare opportunity for high-salary staff
with rare gifts to produce something extraordinary.

A counterproof will be programs proven correct
that are both not rare and also practical.

Re: Tests in a software release

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:osvvds$s97$1@gioia.aioe.org...
...
> No. The contract requires Constraint_Error propagation. Disabling checks 
> breaks that.

I agree.

> The intention of allowing checks being disabled was to allow manual 
> optimization in very few cases when the preconditions are known to be 
> stronger than specified. The source of this knowledge is unknown, it is up 
> to the code maintainer to assert it. For this reason disabling checks 
> cannot be the rule in contrary to what Victor suggested.

I think the main reason for allowing disabling checks had to do with the 
practicalities of computer systems in the late 1970's and early 1980's when 
this part of Ada was originally defined. Back then, memory and CPU time was 
at a premium, optimization technology (especially that regarding checks, 
which few languages had) was not very advanced, and disabling checks could 
make the difference between being able to run a program and not.

Early versions of Janus/Ada disabled all checks just so that more space was 
available for symbols (the first CP/M versions of Janus/Ada had only 56K of 
RAM to run in!).

But in modern compilers, optimization technology is much more advanced, 
checking optimization is something that hundreds of man hours has been spent 
on in every Ada compiler, there is plenty of CPU for general computation, so 
checks should be disabled only in very limited contexts if at all.

Pretty much I only know of three cases: (1) profiling has shown that a 
particular routine is too slow, and suppressing checks for that single 
routine improves the performance of the application; (2) a tool like SPARK 
has been used to prove exception absence for a program with detailed 
code-level verification requirements; suppressing the checks that raise 
those exceptions already proved to be absent cuts the verification 
requirements; (3) a routine implementing something like saturation math is 
being implemented, and suppressing the range and overflow checks makes a 
cheaper implementation.

And personally think that (1) and (2) are better handled in the compiler by 
careful use of subtypes (and in the case of (2), additional warnings if an 
unexpected check is generated). And it's really unclear if (3) is better 
than just handling the exception(s) (and using Unsuppress to ensure no one 
turns off the checks).

Thus I think all style guides should treat pragma Suppress much like Goto 
and Abort, requiring a detailed justification for any usage at all. (Indeed, 
I'd much rather use a Goto, it's much less likely to cause a problem.)

                                           Randy.

Re: Tests in a software release

[Randy Brukardt]

"G.B." <bauhaus@notmyhomepage.invalid> wrote in message 
news:ot981s$7m5$1@dont-email.me...
...
> Checking is behavior. However, let SPARK check conditions
> of a contract, and let the result be Truth. Then they
> have been checked before the program even runs, and
> turning *off* Ada checks is, therefore, justified.

Yes, but a compiler can do this better, since it knows the actual 
representations chosen (which might ensure that a check cannot fail where 
SPARK may not be able to prove this, at least not without lots of additional 
information). Moreover, a compiler surely knows if it generated code to 
raise Constraint_Error.

Ergo, I would much prefer to trust the compiler (and if you can't trust your 
compiler, you have a serious problem that no other tool is going to be able 
to help with) rather than having to trust an entire chain of tools that 
necessarily has to include the compiler.

There are lots of things that SPARK can prove that a compiler can't, but 
there aren't many (if any) check eliminations that require the power of 
SPARK (and I believe that the vast majority of those can be fixed with the 
addition of additional tests or subtypes).

                                  Randy.

Re: Tests in a software release

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:ot9cfr$1k6s$1@gioia.aioe.org...
...
> Ada could have a pragma to remove all ELSE parts of all IF-statements. 
> Would anybody argue for that? (:-))

I'd consider making an argument for a pragma to *require* an ELSE part for 
all IF statements.

The Janus/Ada style guide requires either than ELSE part or a comment 
starting -- Else before the END IF to explain why it isn't needed. We 
adopted that after a string of bugs where there was an If statement without 
an else where it appeared that no one had considered what to do if the IF 
was False. By requiring at least a comment, we make the programmer (often 
me!) think about that case.

Yes, sometimes, they end up being something like:

    -- else *** not sure what to do here!! ***

but at least that is a red flag to anyone looking at the code in a debugging 
situation.

                                Randy.

Re: Tests in a software release

[Randy Brukardt]

"G.B." <bauhaus@notmyhomepage.invalid> wrote in message 
news:oth5k4$eih$1@dont-email.me...
...
>> Checks can be removed only when statically proven not to fail.
>
> Programmers may remove checks whenever they think
> they should. No fancy proof is required(*).

Such programmers should be fired at the earliest opportunity. That turns Ada 
into an inferior version of C.

Such removal probably would have no impact on performance (can even harm it 
in some cases by preventing the removal of other checks), and just makes the 
code much less safe.

                    Randy.

P.S. Can you tell this is a hot button issue for me; I'm answering a stupid 
thread from almost a month ago!!

Re: Tests in a software release

[Dmitry A. Kazakov]

On 15/11/2017 01:06, Randy Brukardt wrote:

> I'd consider making an argument for a pragma to *require* an ELSE part for
> all IF statements.

Only if return and raise statements had the forms:

    return Result when Condition;

    raise Exception with Text when Condition;

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

Re: Tests in a software release

[Jeffrey R. Carter]

On 11/15/2017 01:06 AM, Randy Brukardt wrote:
> 
> I'd consider making an argument for a pragma to *require* an ELSE part for
> all IF statements.

I don't completely agree; I don't think there's a need for an else part for

if C then
    return;
end if;

The idea that the programmer should show that the else processing has been 
considered and deliberately ommitted is good for most if statemwents, though. I 
follow the rule that an if with an elsif part must have an else part. When 
there's multiple branches it's important to show that you've considered them all.

-- 
Jeff Carter
"Who wears beige to a bank robbery?"
Take the Money and Run
144

Re: Tests in a software release

[J-P. Rosen]

> On 11/15/2017 01:06 AM, Randy Brukardt wrote:
>>
>> I'd consider making an argument for a pragma to *require* an ELSE part
>> for
>> all IF statements.
> 
AdaControl:
check statements (no_else);

-- 
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: Tests in a software release

[G. B.]

Randy Brukardt <randy@rrsoftware.com> wrote:
> "G.B." <bauhaus@notmyhomepage.invalid> wrote in message 
> news:oth5k4$eih$1@dont-email.me...
> ...
>>> Checks can be removed only when statically proven not to fail.
>> 
>> Programmers may remove checks whenever they think
>> they should. No fancy proof is required(*).
> 
> Such programmers should be fired at the earliest opportunity.

When I, the programer who knows he is obeying
the clause of the contract that my company and
the supplier‘s have both signed (sic), then the
other party insisting that we should nevertheless 
run their checks does not abide.

And is giving an interesting impression of their
understanding of both contracts and quality.

> That turns Ada 
> into an inferior version of C.

Contracts remove needs for talking about 
what can so easily go wrong in C, because that
has already been talked about and written down
as a contract clause. Ada types and compilers
do help, but only so much.

The most important thing is, designing by contract 
is *not* programming defensively. By definition.

Re: Tests in a software release

[Dmitry A. Kazakov]

On 2017-11-15 17:59, J-P. Rosen wrote:
>> On 11/15/2017 01:06 AM, Randy Brukardt wrote:
>>>
>>> I'd consider making an argument for a pragma to *require* an ELSE part
>>> for all IF statements.
>>
> AdaControl:
> check statements (no_else);

How about a pragma for AdaControl directives [or other verification 
tool] to be called by the compiler?

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

Re: Tests in a software release

[Dmitry A. Kazakov]

On 2017-11-15 18:57, G. B. wrote:

> The most important thing is, designing by contract
> is *not* programming defensively.

It exactly is. In both cases no assumptions beyond known preconditions 
are made. Ada was especially designed to uphold defensive programming. 
E.g. case requires others alternative:

    I : Positive := 1;

    case I is
       when 1 =>
          ...
       when others => -- Defensive and mandatory
          ...
    end case;

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

Re: Tests in a software release

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:ouguv4$1h92$1@gioia.aioe.org...
> On 15/11/2017 01:06, Randy Brukardt wrote:
>
>> I'd consider making an argument for a pragma to *require* an ELSE part 
>> for
>> all IF statements.
>
> Only if return and raise statements had the forms:
>
>    return Result when Condition;
>
>    raise Exception with Text when Condition;

You're right that sometimes the comment isn't very enlightening:

     if Condition then
         return Result;
     -- else nothing needed.
     end if;

...but note that often in such cases it is useful to say how the result will 
be determined if Condition is False:

    -- else continue looking for the result.

which does provide useful information to a reader (especially one that 
hasn't looked at a particular subprogram in a decade, something that happens 
a lot when debugging a long-lived program like Janus/Ada).

The place where this comment is annoying is for tracing:

    if J2Trace.Trace(This_Unit) then
        Put_Line ("Type " & Type_Ptr'Image(The_Type) & " is unconstrained");
    -- else no trace needed.
    end if;

Here, the else comment is noise. I personally usually leave it out (having 
an exception in the style guide for trace messages), but others (especially 
Isaac) always followed the rule religiously, so Janus/Ada is full of this 
comment.

                              Randy.

Re: Tests in a software release

[Randy Brukardt]

"J-P. Rosen" <rosen@adalog.fr> wrote in message 
news:oui2vb$5n2$1@dont-email.me...
>> On 11/15/2017 01:06 AM, Randy Brukardt wrote:
>>>
>>> I'd consider making an argument for a pragma to *require* an ELSE part
>>> for
>>> all IF statements.
>>
> AdaControl:
> check statements (no_else);

I don't think that allows a comment starting with "else" in place of the 
else part. I think that is relatively important, as requiring an empty else 
adds even more text and thus makes the code harder to read.

That is:

    if Condition then
        return Result;
    -- else continue looking for the correct result.
    end if;

compared to:

    if Condition then
        return Result;
    else
        null; -- Continue looking for the correct result.
    end if;

[Also, the null statement might generate some extra code in the form of an 
extra jump if optimization is turned completely off.]

                                                        Randy.

Re: Tests in a software release

[Randy Brukardt]

"G. B." <nonlegitur@nmhp.invalid> wrote in message 
news:ouhv6m$cig$1@dont-email.me...
> Randy Brukardt <randy@rrsoftware.com> wrote:
>> "G.B." <bauhaus@notmyhomepage.invalid> wrote in message
>> news:oth5k4$eih$1@dont-email.me...
>> ...
>>>> Checks can be removed only when statically proven not to fail.
>>>
>>> Programmers may remove checks whenever they think
>>> they should. No fancy proof is required(*).
>>
>> Such programmers should be fired at the earliest opportunity.
>
> When I, the programer who knows he is obeying
> the clause of the contract that my company and
> the supplier's have both signed (sic), then the
> other party insisting that we should nevertheless
> run their checks does not abide.

I hope I never have to use a product that is purposely designed to be 
garbage.

...
> The most important thing is, designing by contract
> is *not* programming defensively. By definition.

One *always* programs defensively. The compiler can eliminate the vast 
majority of the cost automatically, and what it can't eliminate demonstrates 
likely bugs. I'm aggresively pushing Janus/Ada in this direction (don't have 
enough free time to make a lot of progress though), as it combines the 
advantages of what CodePeer does with what an Ada compiler can do, without 
the possible disconnect of having different tools (which necessarily have to 
make assumptions about how the others work).

The easiest level of that is described in an RR blog post from last June: 
http://www.rrsoftware.com/html/blog/quality.html.

I'm working on some additional even more aggresive quality checks; I'll 
write a blog post on them when they're finished, hopefully sometime this 
winter. Ultimately, I'd like to include all checks and contracts in the 
quality checks, but that's going to require a lot of development time and 
probably will appear over multiple years and compiler versions.

In any case, this is the exact opposite of the sort of approach that you are 
championing. It defeats the purpose of Ada, and it doesn't help that the 
client (in your scenario) is asking you to do that. It's still silly.

                                         Randy.

Re: Tests in a software release

[J-P. Rosen]

Le 15/11/2017 à 22:58, Randy Brukardt a écrit :
> I don't think that allows a comment starting with "else" in place of the 
> else part. I think that is relatively important, as requiring an empty else 
> adds even more text and thus makes the code harder to read.
Right, but this could be added. As well as many other things. Want to
see my todo list? Of course, if you have some funding available... ;-)

-- 
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: Tests in a software release

[Robert Eachus]

On Saturday, October 28, 2017 at 3:35:21 AM UTC-4, Dmitry A. Kazakov wrote:
> On 2017-10-28 08:53, G.B. wrote:
> > On 27.10.17 20:54, Dmitry A. Kazakov wrote:
> >> The contract requires Constraint_Error propagation.
> > 
> > Checks require Constraint_Error propagation.
> 
> Checks ensure Constraint_Error as a part of implementation.

It is worth remembering that there are checks for conditions which do not raise Constraint_Error.  I actually used a Suppress for elaboration checks once.  ;-)  There was a call in a function body that could only occur after elaboration was complete, but the compiler couldn't find a valid elaboration order without the Suppress.  It has been decades, so I can't remember the details.

On a related issue, the need for gotos seems to be limited to implementations of finite state machines (FSMs).  I guess I could write a program that would generate goto-less code for deterministic FSMs, For non-deterministic FSMs, I guess the way to go would be to turn them into deterministic FSMs.  Maintaining such code would be next to impossible.

Re: Tests in a software release

[G.B.]

On 15.11.17 23:17, Randy Brukardt wrote:

> ...
>> The most important thing is, designing by contract
>> is *not* programming defensively. By definition.
> 
> One *always* programs defensively.

Why would that be?

FTR, and for what the definitions are,
  http://se.ethz.ch/~meyer/publications/computer/contract.pdf

Referring to some notes from your blog, you cannot always

   - compute things at compile time, hoping to optimize;
   - perform run-time checks in a timely fashion, without
     checks causing timeouts:

     function Binary_Search (X : List_of_Things) return Thing;
     --  ... provided that elements of X are ordered by "<=".
  

     procedure Foo (X : Graph; P : Node_Process);
     --  ... provided that X is a DAG.


Is_Sorted can be expressed in Ada, but the compiler cannot
prove this at run-time, foreseeing data that are becoming
available only then. It has no say, at that point.

Similarly, Is_Dag cannot be computed at compile time.
Checking Is_Dag at run-time will be prohibitively
expensive at Foo's end. Still checking is Bad Design, as
Dmitry might possibly put it, I guess, because a DAG is
a DAG by construction. At run-time.

So, what needs to be done and what is usually done
is that clients will be sure to call subprograms
passing sorted lists and passing DAGs, resp. No checks,
no defenses, just doing what the contract says we should.

So, while no compiler can eliminate the computations for
the reasons stated ("optimize"), we can if our code abides,
by *not* having Binary_Search *check* proper ordering.

Thus, your future compiler could not "demonstrate likely
bugs" for these contracts, but if the optimizer fails at
predicting all run-time values in X and therefore adds checks,
it likely prevents efficient real-time computation for the
contracts outlined above.

> In any case, this is the exact opposite of the sort of approach that you are
> championing.

On the contrary: you write the contract's clauses of
all parties to your compiler and then, once you
know your code meets the requirements of the contracts,
you drop checking code accordingly ("optimize") and in
good conscience.

    if X /= X or else X /= X then

       --  what, at compile time,
       --  for which which kind of X?

Re: Tests in a software release

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 693 bytes --]

"J-P. Rosen" <rosen@adalog.fr> wrote in message 
news:ouj8vg$dvp$1@dont-email.me...
> Le 15/11/2017 à 22:58, Randy Brukardt a écrit :
>> I don't think that allows a comment starting with "else" in place of the
>> else part. I think that is relatively important, as requiring an empty 
>> else
>> adds even more text and thus makes the code harder to read.
> Right, but this could be added. As well as many other things. Want to
> see my todo list? Of course, if you have some funding available... ;-)

Of course, everything can be done with funding (and/or time). I've got a 
zillion good ideas that I don't have the time/money to implement.

                                         Randy.

Re: Tests in a software release

[Randy Brukardt]

"G.B." <bauhaus@notmyhomepage.invalid> wrote in message 
news:oul0ra$jee$1@dont-email.me...
> On 15.11.17 23:17, Randy Brukardt wrote:
>
>> ...
>>> The most important thing is, designing by contract
>>> is *not* programming defensively. By definition.
>>
>> One *always* programs defensively.
>
> Why would that be?

Because the real world is a nasty place where unexpected things go wrong. 
The fewer assumptions a human has to make, the the better. A computer 
program can handle making assumptions much better, because it can juggle 
many of them and will not get confused.




> FTR, and for what the definitions are,
>  http://se.ethz.ch/~meyer/publications/computer/contract.pdf
>
> Referring to some notes from your blog, you cannot always
>
>   - compute things at compile time, hoping to optimize;
>   - perform run-time checks in a timely fashion, without
>     checks causing timeouts:

My blog was exclusively talking about language-defined constructs and 
checks. None of the rules described in the blog have any effect on 
user-defined operators (that is, ordinary function calls) because the 
compiler cannot know what the body does. Indeed, my entire discussion here 
has been about pragma Suppress and does not necessarily apply to 
user-defined contracts (that is, pragma Assertion_Policy as applies to 
things like Pre and Post).

There is absolutely no connection between pragma Suppress and pragma 
Assertion_Policy in Ada -- they work entirely differently 
(Assertion_Policy(Ignore) cannot by itself cause erroneous execution, while 
pragma Suppress almost always can).

A lot can be done with user-defined contracts, but that depends on contract 
aspects not defined in Ada 2012 (like Global, which hopefully will be in Ada 
2020). As you note correctly, timing issues might still require using 
Ignore, since it is easy to write very expensive predicates that cannot be 
left in a production system.

I believe that latter problem is a flaw in the contract system as written; 
most predicates are *not* expensive (think Is_Open in Text_IO) and thus have 
no need to be Ignored; it would be best if the occassional expensive 
predicate could be flagged and only those ignored. But again, none of that 
has anything to do with what I was discussing.

...
> On the contrary: you write the contract's clauses of
> all parties to your compiler and then, once you
> know your code meets the requirements of the contracts,
> you drop checking code accordingly ("optimize") and in
> good conscience.

Never for language-defined checks; there is no point as any barely competent 
compiler will drop them automatically for free. If it can't drop them, it's 
highly likely that your code has a bug. User-defined contracts are a 
different deal; I'd prefer to never eliminate them, either, but I recognize 
that a few are going to be too expensive, and it's not as clear that the 
compiler will be able to optimize them (although in many cases, it will be 
able to do so to get sufficient performance).

...
>    if X /= X or else X /= X then
>
>       --  what, at compile time,
>       --  for which which kind of X?

This is dubious for *ANY* kind of X. This is just a warning because X might 
be something with a side-effect and thus this might actually mean something 
other than the nothing that it appears to mean -- but even in such a case, 
the code is clearly tricky and it would be better written some other way 
that is less tricky to a reader that doesn't necessarily know the details of 
X.

This is all explained in detail in the blog and I'm not sure why you are 
asking about it here.

                                              Randy.

Re: Tests in a software release

[Randy Brukardt]

"Robert Eachus" <rieachus@comcast.net> wrote in message 
news:920c1eff-2cfa-48d4-a0a7-6b6f0a205ce5@googlegroups.com...
...
>On a related issue, the need for gotos seems to be limited to 
>implementations of
>finite state machines (FSMs).  I guess I could write a program that would 
>generate
>goto-less code for deterministic FSMs, For non-deterministic FSMs, I guess 
>the
>way to go would be to turn them into deterministic FSMs.  Maintaining such 
>code
>would be next to impossible.

The main reason to use a goto in Ada 2012 is for the (missing) loop continue 
statement. I do this quite often (and so does the GNAT code, if I'm 
remembering correctly) -- real code being much more complex than this:

     loop
         ...
         if ...
            ...
            goto Continue; -- Start next iteration.
         end if;
         ...
         <<Continue>>
     end loop;

Note that Ada 2012 eliminated the need for "null;" after a label 
specifically so that this usage would read better.

                                Randy.

Re: Tests in a software release

[Shark8]

On Wednesday, November 15, 2017 at 1:46:35 PM UTC-7, Dmitry A. Kazakov wrote:
> On 2017-11-15 18:57, G. B. wrote:
> 
> > The most important thing is, designing by contract
> > is *not* programming defensively.
> 
> It exactly is. In both cases no assumptions beyond known preconditions 
> are made. Ada was especially designed to uphold defensive programming. 
> E.g. case requires others alternative:
> 
>     I : Positive := 1;
> 
>     case I is
>        when 1 =>
>           ...
>        when others => -- Defensive and mandatory
>           ...
>     end case;

Except that Ada allows CASE to be non-defensive and natural operation over sets:

Example : Integer with Import, Address => SOME_PORT;

Subtype Negative is Integer range Integer'First..Integer'Pred(Natural'First);
Subtype Small_Prime is Positive range Positive'Succ(Positive'First)..2**5
  with Static_Predicate => Small_Prime in
       2 | 3 | 5 | 7 | 11 | 13 | 17 | 19 | 23 | 29 | 31;

Case Example is
  when Negative    => Do_Negative;
  when 0           => Do_Zero;
  when 1           => Do_One;
  when Small_Prime => Do_Prime;
  when others      => Do_Positive_General;
End Case;

Re: Tests in a software release

[Shark8]

On Thursday, November 16, 2017 at 2:44:12 PM UTC-7, G.B. wrote:
> 
> On the contrary: you write the contract's clauses of
> all parties to your compiler and then, once you
> know your code meets the requirements of the contracts,
> you drop checking code accordingly ("optimize") and in
> good conscience.
> 
>     if X /= X or else X /= X then
> 
>        --  what, at compile time,
>        --  for which which kind of X?

IEEE754's NaN would yield true in that case, so you can't simply optimize that away, you'd have to do some analysis of the "="/"/=" operator.

Re: Tests in a software release

[Randy Brukardt]

"Shark8" <onewingedshark@gmail.com> wrote in message 
news:12f75e44-f61b-4b59-ab82-3ae9b151f0be@googlegroups.com...
> On Thursday, November 16, 2017 at 2:44:12 PM UTC-7, G.B. wrote:
>>
>> On the contrary: you write the contract's clauses of
>> all parties to your compiler and then, once you
>> know your code meets the requirements of the contracts,
>> you drop checking code accordingly ("optimize") and in
>> good conscience.
>>
>>     if X /= X or else X /= X then
>>
>>        --  what, at compile time,
>>        --  for which which kind of X?
>
> IEEE754's NaN would yield true in that case, so you can't simply
> optimize that away, you'd have to do some analysis of the "="/"/="
> operator.

(1) This is not an optimization, it is a Code Quality Warning. Code like the 
above is either impossibly tricky or is some sort of mistake. But the 
compiler doesn't change any code to something else in these cases, it 
expects the programmer to fix their bug. There's no way that the compiler 
can guess (in general) what mistake the programmer made.

The classic example for this sort of case mentioned in the blog is:
    for I in Arr'range loop
        for J in Arr'range loop
              if Arr(I) = Arr(I) then -- !!
                  ...

Here, one gets a Code Quality Warning as the condition is always True. It's 
pretty obvious that the second (I) in the condition is supposed to be a (J), 
but that's obvious to a human, not to a compiler.

(2) But we could make that optimization if we wanted to, a NAN is invalid. 
And operations on an invalid value are implementation-defined (if 
Constraint_Erorr or Program_Error is not raised). Ergo, no one can make any 
assumptions about them. And a compiler can do anything it wants (including 
making the optimization you suggest work).

Janus/Ada specifically makes no attempt to preserve any IEEE math (it looks 
insane to me) - we only worry about meeting the Annex G requirements of Ada. 
If you truly need IEEE math, you'll have to use some other Ada compiler.

(As always, some customer could show up with enough money to encourage me to 
care, but that hasn't happened to date.)

(3) Janus/Ada does essentially no floating point optimizations because 
pretty much anything runs afoul of accuracy problems. That means it has 
terrible floating point performance (again, something that hasn't mattered 
to our customers in general). I recently recompiled a float intensive 
Janus/Ada program with GNAT, and the runtime of approximately 48 hours with 
Janus/Ada dropped to about 30 minutes with GNAT. (Needless to say, I've 
stopped using the Janus/Ada version of that program.)

Again, if we had customers for which this mattered a lot, we'd work on it, 
but that hasn't been true to date and there are a lot of other things 
competing for our time.

                                        Randy.

Re: Tests in a software release

[Robert Eachus]

On Thursday, November 16, 2017 at 7:20:22 PM UTC-5, Randy Brukardt wrote:

> The main reason to use a goto in Ada 2012 is for the (missing) loop 
> continue statement. I do this quite often (and so does the GNAT code,
> if I'm remembering correctly) -- real code being much more complex
> than this:

>     loop 
>         ... 
>        if ... 
>            ... 
>            goto Continue; -- Start next iteration. 
>        end if; 
>         ... 
>         <<Continue>> 
>     end loop; 

Shrug. Even if the loop is intended to run until the power shuts off--an example is the flight control software for an airplane--that construct clearly implements a finite state machine, and I'd probably include the FSM in the documentation.  I'd definitely include the FSM if there is another way out of that loop other than power failing usually one or more return statements. One or more exceptions can do the same thing, and it helps to document how you can get to the exception handler from the loop.

And by 'it helps' I don't mean only during maintenance.  I've spent days working back and forth from the documentation to the source code until they agreed, and agreed with the requirements.

More simply said, most FSMs in Ada are implemented as loops without for or while clauses.  The alternative has a label at the entrance and several gotos
back to it.