Browse Prior Art Database

A PROCEDURE CALL PROOF RULE (WITH A SIMPLE EXPLANATION)

IP.com Disclosure Number: IPCOM000148269D
Original Publication Date: 1979-May-31
Included in the Prior Art Database: 2007-Mar-29

Publishing Venue

Software Patent Institute

Related People

Gries, David: AUTHOR [+3]

Abstract

1. I n t r o d u c t i o n We p r e s e n t a procedure c a l l proof r u l e f o r a language w i t h a one-dimensional a r r a y s and r e c o r d s , i n which a r r a y e l e ments and r e c o r d f i e l d s may themselves be a r r a y s o r r e c o r d s ; p o i n t e r s a r e not allowed;' b prncedures with g l o b a l v a r i a b l e s , var c a l l by r e f e r e n c e parameters, and ALGOL 60 v a l u e parameters; (c) procedure c a l l s i n which no a l i a s i n g is allowed among t h e g l o b a l v a r i a b l e s and var arguments, b u t no r P s t r i c t i o n is placed on v a l u e arguments, d l no r e c u r s i o n , although it could be introduced w i t h little d i f f i c u l t y . An attempt is made t o keep t h e n o t a t i o n a s simple as p o s s i b l e and t o make t h e proof r u l e as c l e a r and understandable a s p a s s i ble. We w i l l , at t h e end o f t h i s r e p o r t , compare b r i e f l y t h i s proof r u l e w i t h o t h e r s found i n t h e l i t e r a t u r e . Also aDpearing i n t h i s r e p o r t is a d e f i n i t i o n o f m u l t i p l e assign~nent. T h i s is given because t h e concept is necessary for understanding procedure c a l l s , and a l s o because t h e d e f i n i t i o n is much simpler, s h o r t e r and more g e n e r a l th,an t h e one p r e v i o u s l y published by t h e first a u t h o r 143.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 13% of the total text.

Page 1 of 16

[This page contains 1 picture or other non-text object]

Page 2 of 16

[This page contains 1 picture or other non-text object]

Page 3 of 16

1. I n t r o d u c t i o n


We p r e s e n t a procedure c a l l proof r u l e f o r a language w i t h ( a ) one-dimensional a r r a y s and r e c o r d s , i n which a r r a y e l e - ments and r e c o r d f i e l d s may themselves be a r r a y s o r r e c o r d s ; p o i n t e r s a r e not allowed;' ( b ) prncedures with g l o b a l v a r i a b l e s , var ( c a l l by r e f e r e n c e ) parameters, and ALGOL 60 v a l u e parameters;
(c) procedure c a l l s i n which no a l i a s i n g is allowed among t h e g l o b a l v a r i a b l e s and var arguments, b u t no r P s t r i c t i o n is placed on v a l u e arguments, ( d l no r e c u r s i o n , although it could be introduced w i t h little d i f f i c u l t y .

An attempt is made t o keep t h e n o t a t i o n a s simple as p o s s i b l e and t o make t h e proof r u l e as c l e a r and understandable a s p a s s i - ble. We w i l l , at t h e end o f t h i s r e p o r t , compare b r i e f l y t h i s proof r u l e w i t h o t h e r s found i n t h e l i t e r a t u r e .

     Also aDpearing i n t h i s r e p o r t is a d e f i n i t i o n o f m u l t i p l e assign~nent. T h i s is given because t h e concept is necessary for understanding procedure c a l l s , and a l s o because t h e d e f i n i t i o n
is much simpler, s h o r t e r and more g e n e r a l th,an t h e one p r e v i o u s l y published by t h e first a u t h o r 143.

     Procedure c a l l s w i t h a l i a s i n g w i l l be d i s c u s s e d , and an i d e a w i l l be o u t l i n e d f o r a d e f i n i t i o n of such calls t h a t r e f l e c t s t h e n o t i o n t h a t such a l i a s i n g , while perhaps u s e f u l a t times, should be t r e a t e d a s a s e p a r a t e , s p e c i a l case.

2. References a ~ d
a l i a s i n q

     Consider a " v a r i a b l e " I,ike b t i 3 .s, where b is an a r r a y of r e c o r d s w i t h f i e l d s. Such a r e f e r e n c e , as w e w i l l c a l l it, c o n s i s t s of an i d e n t i f i e r -- b -- concatenated w i t h a ( p o s s i b l y n u l l ) s e l e c t o r -- Ii1.s -- which is e s s e n t i a l l y a sequence o f s u b s c r i p t s and Yield names. The symbol d e n o t e s t h e n u l l s e l e c t o r . The symbol o w i l l be used from time t o t i m s t o den- o t e c o n c a t e n a t i o n of i d e n t i f i e r s and s e l e c t o r s -- u s u a l l y when i d e n t i f i e r s a r e used t o r e p r e s e n t a r b i t r a r y s e l e c t o r s , e.g.

b a s l o s 2 . kote a l s o t h a t b = bee.

[This page contains 1 picture or other non-text object]

Page 4 of 16

     Two references are a l i a s e d i f one is an i n i t i a l segment of t h e other, which means t h a t t h e latterlreferen...