From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,ae9506fd4dcf7090
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2002-10-23 01:39:58 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news.tele.dk!news.tele.dk!small.news.tele.dk!fu-berlin.de!uni-berlin.de!tar-alcarin.cbb-automation.DE!not-for-mail
From: Dmitry A. Kazakov <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Concatenation and Characters
Date: Wed, 23 Oct 2002 10:39:56 +0200
Message-ID: <i3ncruorrn9nb7c5ce88avqperg3ffr50c@4ax.com>
References: <ysgp9.714$_u6.401@nwrddc01.gnilink.net>
 <3ZTs9.1528$Bd4.11780@dfw-service2.ext.raytheon.com>
 <n658ru0mdrqfl6d4k3f9htvkfcku64muok@4ax.com>
 <ap1l37$mbh$1@a1-hrz.uni-duisburg.de>
 <ap381k$qlpkr$1@ID-77047.news.dfncis.de>
 <ap3eu7$3r2$3@a1-hrz.uni-duisburg.de>
NNTP-Posting-Host: tar-alcarin.cbb-automation.de (212.79.194.111)
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
X-Trace: fu-berlin.de 1035362397 29413869 212.79.194.111 (16 [77047])
X-Newsreader: Forte Agent 1.8/32.548
Xref: archiver1.google.com comp.lang.ada:30060
Date: 2002-10-23T10:39:56+02:00
List-Id: <comp.lang.ada>

On Tue, 22 Oct 2002 12:05:27 +0000 (UTC), Georg Bauhaus
<sb463ba@l1-hrz.uni-duisburg.de> wrote:

>Dmitry A.Kazakov <mailbox@dmitry-kazakov.de> wrote:
>: Secondly, your example refers to program semantics, not syntax. Semantics 
>: cannot be checked or verified neither formally nor by a human being.
>
>Hmmm....  Wasn't there something in SPARK...

semantics check => halting problem

>: One of 
>: good ideas of Ada design as I see it, was to *syntactically* mark the 
>: constructs which are potentially dangerous, make them visible for both who 
>: writes and who reads the program.
>
>o.K. it is not built into the language, but a syntactically valid
>subprogram a la
>
>  procedure fill(bowl: out glass; filled: out boolean);
>
>does inform readers about a potentially unsatisfying dring?

No. [ Of course, one could write an appropriate comment, but this sort
of things can be well applied to any language even to ugly C++.]

In this case "bowl" and "filled" have different semantics. "bowl" can
be left uninitailized (I assume that "glass" isn't controlled),
"filled" shall be always set. So I wished that this difference would
be exposed through the syntax. Which way, it is another question. It
could be for example:

procedure fill(bowl: out glass := <>; filled: out boolean := True);

Here I see from the spec, that bowl could be possibly invalid.

Should I write:

procedure fill(bowl: out glass; filled: out boolean);

then the compiler would complain that this form of parameter
specification is allowed for only the types having initial values.

---
Regards,
Dmitry Kazakov
www.dmitry-kazakov.de