Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10 5/3/83; site bmcg.UUCP
Path: utzoo!linus!security!genrad!decvax!ittvax!dcdwest!sdcsvax!bmcg!bprice
From: bprice@bmcg.UUCP
Newsgroups: net.lang
Subject: Re: Strong Typing and Ignorance
Message-ID: <685@bmcg.UUCP>
Date: Mon, 12-Dec-83 12:42:54 EST
Article-I.D.: bmcg.685
Posted: Mon Dec 12 12:42:54 1983
Date-Received: Wed, 14-Dec-83 01:34:11 EST
References: <2892@utcsrgv.UUCP> <137@csd1.UUCP>, <1457@rlgvax.UUCP>
Organization: Burroughs Corporation, San Diego
Lines: 51

<inedible line for voracious mailers>

Thank you for asking the question--it brings up one of the advantages of 
Pascal's variable-oriented strong typing, as opposed to Lisp's form.  The
particular advantage is that the typing is an assertion that is to be used
in a partial correctness-proof.

>From: guy@rlgvax.UUCP
>Organization: CCI Office Systems Group, Reston, VA
>A sidenote to the article by Michael Condict:
>He mentions that the assignment of an integer to a subrange-typed variable
>requires runtime checking.  Has any work been done on proving such assignments
>correct given constraints on the values assumed by the integers in question?
>I.e., if you have

>procedure foo(var i, j : integer);
>var k : 2 .. 12;
>    begin
>       { ASSERT 1 <= i <= 6, 1 <= j <= 6 }
>       k = i + j;
>    end

>if the assertion in question is true, 2 <= i+j <= 12 so the assignment
>will always be valid.

>      Guy Harris

Work has been done on the question, although most that I know of has cast
the assertion in Pascal form.  The subrange assertion in the comment of your
example carries exactly the information conveyed by subrange-type, so if we
rewrite the example:

type halfdozenorless: 1..6;
...
procedure foo(var i, j : halfdozenorless);
var k : 2 .. 12;
    begin
       k := i + j;
    end

then we have the assertion in the standard Pascal form.

Jim Welsh (Economic Range Checks in Pascal, S-P&E 8 pp85-97, 1978) observes
that many examples, like this one, have enough information that run-time
range-checking cannot be violated.  He reports on an implementation.  
Several other implementations exist now--I think the next CDC release will
include this improvement, but don't count on my fallible word.  I did an
implementation, too, for the DECSystem-10.
-- 
--Bill Price    uucp:   {decvax!ucbvax  philabs}!sdcsvax!bmcg!bprice
                arpa:?  sdcsvax!bmcg!bprice@nosc