Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.1a 12/4/83; site rlgvax.UUCP
Path: utzoo!linus!security!genrad!decvax!harpo!seismo!rlgvax!guy
From: guy@rlgvax.UUCP (Guy Harris)
Newsgroups: net.lang
Subject: Re: Strong Typing and Ignorance
Message-ID: <1457@rlgvax.UUCP>
Date: Wed, 7-Dec-83 00:46:59 EST
Article-I.D.: rlgvax.1457
Posted: Wed Dec  7 00:46:59 1983
Date-Received: Fri, 9-Dec-83 05:20:59 EST
References: <2892@utcsrgv.UUCP> <137@csd1.UUCP>
Organization: CCI Office Systems Group, Reston, VA
Lines: 21

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
	{seismo,ihnp4,allegra}!rlgvax!guy