States, side effects and multiple contexts in programming languages

Graduation date: 1985In von Neumann Languages, side effects occur if one or more non local variables change value(s) during the execution of a procedure or a function. Side effects can occur only if the programming language provides a notion of memory (or state) where the effect will be stored. Side effects complicate the semantics of such languages. As a result programs are often hard to prove or verify in languages permitting side effects. The applicative languages eliminate the problem of side effects altogether by removing the concept of memory or state. Consequently,these languages have simpler semantics and applicative programs are easier to to prove. In this thesis we explore the design of the programming language EML ( for Environment Modeling Language). EML retains the the notion of memory and restricts but does not eliminate side effects. Restriction of side effects is enforced by eliminating the notion of global accessibility to a data item and by the introducing the concept of a 'consumable' variable. In this model a variable once accessed by a procedure is assumed to be consumed in the calling environment. A consumed variable may not be used by any other procedure till its value is regenerated by the execution of some other procedure. Instead of global accessibility, in EML data exchange is limited only between neighboring environments, i.e an EML procedure can accept and return data only to the procedure which invokes it. We show that these restrictions simplify the semantics of assignment based languages and improve the provability of EML programs. An approach to verifying EML programs employing the notion of equivalent function is discussed. EML should be useful for programming and verifying properties of programs intended to model and manipulate environments