[go: up one dir, main page]

0% found this document useful (0 votes)
77 views17 pages

PPL 1

Java has five Imperative Core constructs: assignment, variable declaration, sequence, test, and loop. Imperative Core are all proper Java statements, while y + 3 = x; x + 2 = y + 5; are not.
Copyright
© Attribution Non-Commercial (BY-NC)
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
0% found this document useful (0 votes)
77 views17 pages

PPL 1

Java has five Imperative Core constructs: assignment, variable declaration, sequence, test, and loop. Imperative Core are all proper Java statements, while y + 3 = x; x + 2 = y + 5; are not.
Copyright
© Attribution Non-Commercial (BY-NC)
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 17

1

Imperative Core

1.1 Five Constructs


Most programming languages have, among others, five constructs: assignment,
variable declaration, sequence, test, and loop. These constructs form the im-
perative core of the language.

1.1.1 Assignment

The assignment construct allows the creation of a statement with a variable x


and an expression t. In Java, this statement is written as x = t;. Variables are
identifiers which are written as one of more letters. Expressions are composed
of variables and constants with operators, such as +, -, *, / — division — and
% — modulo.
Therefore, the following statements
x = y % 3;

x = y;

y = 3;

x = x + 1;

G. Dowek, Principles of Programming Languages, 1


Undergraduate Topics in Computer Science, DOI 10.1007/978-1-84882-032-6_1,

c Springer-Verlag London Limited 2009
2 1. Imperative Core

are all proper Java statements, while


y + 3 = x;

x + 2 = y + 5;
are not.
To understand what happens when you execute the statement x = t; sup-
pose that within the recesses of your computer’s memory, there is a com-
partment labelled x. Executing the statement x = t; consists of filling this
compartment with the value of the expression t. The value previously contained
in compartment x is erased. If the expression t is a constant, for example 3,
its value is the same constant. If it is an expression with no variables, such as
3 + 4, its value is obtained by carrying out mathematical operations, in this
case, addition. If expression t contains variables, the values of these variables
must be looked up in the computer’s memory. The whole of the contents of the
computer’s memory is called a state.
Let us consider, initially, that expressions, such as x + 3, and statements,
such as y = x + 3;, form two disjoint categories. Later, however, we shall be
brought to revise this premise.
In these examples, the values of expressions are integers. Computers can
only store integers within a finite interval. In Java, integers must be between
-231 and 231 - 1, so there are 232 possible values. When a mathematical op-
eration produces a value outside of this interval, the result is kept within the
interval by taking its modulo 232 remainder. Thus, by adding 1 to 231 - 1, that
is to say 2147483647, we leave the interval and then return to it by removing
232 , which gives -231 or -2147483648.
Exercise 1.1
What is the value of the variable x after executing the following state-
ment?

x = 2 * 1500000000;

In Caml, assignment is written x := t. In the expression t, we designate


the value of x, not with the expression x itself, but with the expression !x. Thus,
in Caml we write y := !x + 1 while in Java we write y = x + 1;.
In C, assignment is written as it is in Java.
1.1 Five Constructs 3

1.1.2 Variable Declaration

Before being able to assign values to a variable x, it must be declared, which


associates the name x to a location in the computer’s memory.
Variable declaration is a construct that allows the creation of a statement
composed of a variable, an expression, and a statement. In Java, this statement
is written {int x = t; p} where p is a statement, for example {int x = 4;
x = x + 1;}. The variable x can then be used in the statement p, which is
called the scope of variable x.
It is also possible to declare a variable without giving it an initial value,
for example, {int x; x = y + 4;}. We must of course be careful not to use
a variable which has been declared without an initial value and that has not
been assigned a value. This produces an error.
Apart from the int type, Java has three other integer types that have
different intervals. These types are defined in Table 1.1. When a mathematical
operation produces a value outside of these intervals, the result is returned to
the interval by taking its remainder, modulo the size of the interval.
In Java, there are also other scalar types for decimal numbers, booleans,
and characters. These types are defined in Table 1.1. Operations allowed in the
construction of expressions for each of these types are described in Table 1.2.
Variables can also contain objects that are of composite types, like arrays
and character strings, which we will address later. Because we will need them
shortly, character strings are described briefly in Table 1.3.

The integers are of type byte, short, int or long corresponding to the
intervals [-27 , 27 - 1], [-215 , 215 - 1], [-231 , 231 - 1] and [-263 ,
263 - 1], Respectively. Constants are written in base 10, for example, -666.

Decimal numbers are of type float or double. Constants are written in sci-
entific notation, for example 3.14159, 666 or 6.02E23.

Booleans are of type boolean. Constants are written as false and true.

Characters are of type char. Constants are written between apostrophes, for
example ‘b’.

Table 1.1 Scalars types in Java

To declare a variable of type T, replace the type int with T. The general
form of a declaration is thus {T x = t; p}.
4 1. Imperative Core

The basic operations that allow for arithmetical expressions are +, -, *, /


— division — and % — modulo.

When one of the numbers a or b is negative, the number a / b is the quotient


rounded towards 0. So the result of a / b is the quotient of the absolute values
of a and b, and is positive when a and b have the same sign, and negative if
they have different signs. The number a % b is a - b * (a / b). So (-29) /
4 equals -7 and (-29) % 4 equals -1.

The operations for decimal numbers are +, -, *, /, along with some transcen-
dental functions: Math.sin, Math.cos, ...

The operations allowed in boolean expressions are ==, != — different —, <,


>, <=, >=, & — and —, &&, | — or —, || and ! — not.

For all data types, the expression (b) ? t : u evaluates to the value of t if
the boolean expression b has the value true, and evaluates to the value of u
if the boolean expression b has the value false.

Table 1.2 Expressions in Java

Character strings are of type String. Constants are written inside quotation
marks, for example "Principles of Programming Languages".

Table 1.3 Character strings in Java

In Caml, variable declaration is written as let x = ref t in p and it isn’t


necessary to explicitly declare the variable’s type. It is not possible in Caml to
declare a variable without giving it an initial value.
In C, like in Java, declaration is written {T x = t; p}. It is possible to
declare a variable without giving it an initial value, and in this case, it could
have any value.
In Java and in C, it is impossible to declare the same variable twice, and
the following program is not valid.
int y = 4;
int x = 5;
int x = 6;
y = x;
In contrast, nothing in Caml stops you from writing
1.1 Five Constructs 5

let y = ref 4
in let x = ref 5
in let x = ref 6
in y := !x
and this program assigns the value 6 to the variable y, so it is the most recent
declaration of x that is used. We say that the first declaration of x is hidden by
the second.
Java, Caml and C allow the creation of variables with an initial value that
can never be changed. This type of variable is called a constant variable. A
variable that is not constant is called a mutable variable. Java assumes that
all variables are mutable unless you specify otherwise. To declare a constant
variable in Java, you precede the variable type with the keyword final, for
example
final int x = 4;
y = x + 1;
The following statement is not valid, because an attempt is made to alter the
value of a constant variable
final int x = 4;
x = 5;
In Caml, to indicate that the variable x is a constant variable, write let x
= t in p instead of writing let x = ref t in p. When using constant vari-
ables, you do not write !x to express its value, but simply x. So, you can write
let x = 4 in y := x + 1, while the statement let x = 4 in x := 5 is in-
valid. In C, you indicate that a variable is a constant variable by preceding its
type with the keyword const.

1.1.3 Sequence

A sequence is a construct that allows a single statement to be created out of two


statements p1 and p2 . In Java, a sequence is written as {p1 p2 }. The statement
{p1 {p2 { ... pn } ...}} can also be written as {p1 p2 ... pn }.
To execute the statement {p1 p2 } in the state s, the statement p1 is first
executed in the state s, which produces a new state s’. Then the statement p2
is executed in the state s’.
In Caml, a sequence is written as p1 ; p2 . In C, it is written the same as it
is in Java.
6 1. Imperative Core

1.1.4 Test

A test is a construct that allows the creation of a statement composed of a


boolean expression b and two statements p1 and p2 . In Java, this statement is
written if (b) p1 else p2 .
To execute the statement if (b) p1 else p2 in a state s, the value of
expression b is first computed in the state s, and depending on whether or not
its value is true or false, the statement p1 or p2 is executed in the state s.
In Caml, this statement is written if b then p1 else p2 . In C, it is writ-
ten as it is in Java.

1.1.5 Loop

A loop is a construct that allows the creation of a statement composed of a


boolean expression b and a statement p. In Java, this statement is written
while (b) p.
To execute the statement while (b) p in the state s, the value of b is first
computed in the state s. If this value is false, execution of this statement is
terminated. If the value is true, the statement p is executed, and the value
of b is recomputed in the new state. If this value is false, execution of this
statement is terminated. If the value is true, the statement p is executed, and
the value of b is recomputed in the new state... This process continues until b
evaluates to false.
This construct introduces a new possible behaviour: non-termination. In-
deed, if the boolean value b always evaluates to true, the statement p will
continue to be executed forever, and the statement while (b) p will never
terminate. This is the case with the instruction
int x = 1;
while (x >= 0) {x = 3;}
To understand what is happening, imagine a fictional statement called
skip; that performs no action when executed. You can then define the state-
ment while (b) p as shorthand for the statement
if (b) {p if (b) {p if (b) {p if (b) ...
else skip;}
else skip;}
else skip;}
else skip;
So a loop is one of the ways in which you can express an infinite object using a
1.2 Input and Output 7

finite expression. And the fact that a loop may fail to terminate is a consequence
of the fact that it is an infinite object.
In Caml, this statement is written while b do p. In C, it is written as it
is in Java.

1.2 Input and Output


An input construct allows a language to read values from a keyboard and other
input devices, such as a mouse, disk, a network interface card, etc. An output
construct allows values to be displayed on a screen and outputted to other
peripherals, such as a printer, disk, a network interface card, etc.

1.2.1 Input

Input constructs in Java are fairly complex, so we will use an extension of Java
created specially for this book: the class Ppl1 .
Evaluation of the expression Ppl.readInt() waits for the user to type a
number on her/his keyboard, and returns this number as the value of the
expression. A typical usage is n = Ppl.readInt();. The class Ppl also contains
the construction Ppl.readDouble which allows decimal numbers to be read
from the keyboard, and the construction Ppl.readChar which allows characters
to be read.

1.2.2 Output

Execution of the statement System.out.print(t); outputs the value of ex-


pression t to the screen. Execution of the statement System.out.println();
outputs a newline character that moves the cursor to the next line. Execution
of the statement System.out.println(t); outputs the value of expression t
to the screen, followed by a newline character.
Exercise 1.2
Write a Java program that reads an integer n from the keyboard, com-
putes the value of 2n and outputs it to the screen.
1
The file Ppl.java is available on the author’s web site. Simply place it in the
current directory to use the examples described here.
8 1. Imperative Core

Exercise 1.3
Write a Java program that reads an integer n from the keyboard, and
outputs a boolean indicating whether the number is prime or not.

Graphical constructs that allow drawings to be displayed are fairly complex


in Java. But, the class Ppl contains some simple constructions to produce
graphics. The statement Ppl.initDrawing(s,x,y,w,h); creates a window
with the title s, of width w and of height h, positioned on the screen at co-
ordinates (x,y). The statement Ppl.drawLine(x1,y1,x2,y2); draws a line
segment with endpoints (x1,y1) and (x2,y2). The statement Ppl.drawCircle
(x,y,r); draws a circle with centre (x,y) and with radius r. The state-
ment Ppl.paintCircle(x,y,r); draws a filled circle and the statement
Ppl.eraseCircle(x,y,r); allows you to erase it.

1.3 The Semantics of the Imperative Core


We can, as we have below, express in English what happens when a statement
is executed. While this is possible for the simple examples in this chapter, such
explanations quickly become complicated and imprecise. Therefore, we shall
introduce a theoretical framework that might seem a bit too comprehensive at
first, but its usefulness will become clear shortly.

1.3.1 The Concept of a State

We define an infinite set Var whose elements are called variables. We also define
the set Val of values which are integers, booleans, etc. A state is a function that
associates elements of a finite subset of Var to elements of the set Val.
For example, the state [x = 5, y = 6] associates the value 5 to the vari-
able x and the value 6 to the variable y. On the set of states, we define an
update function + such that the state s + (x = v) is identical to the state s,
except for the variable x, which now becomes associated with the value v. This
operation is always defined, whether x is originally in the domain of s or not.
We can then simply define a function called Θ, which for each pair (t,s)
composed of an expression t and a state s, produces the value of this expression
in this state. For example, Θ(x + 3,[x = 5, y = 6]) = 8.
This is a partial function, because a state is a function with a finite domain
while the set of variables is infinite. For example, the expression z + 3 has no
1.3 The Semantics of the Imperative Core 9

value in the state [x = 5, y = 6]. In practice, this means that attempting


to compute the value of the expression z + 3 in the state [x = 5, y = 6]
produces an error.
Executing a statement within a state produces another state, and we define
what happens when a statement is executed using a function called Σ. Σ has a
statement p, an initial state s and produces a new state, Σ(p,s). This is also
a partial function. Σ(p,s) is undefined when executing the statement p in the
state s produces an error or does not terminate.
In the case of a statement p having the form x = t;, the Σ function is
defined as follows
Σ(x = t;,s) = s + (x = Θ(t,s)).
For example, Σ(x = x + 1;,[x = 5]) = [x = 6]. This is equivalent to
saying ‘Executing the statement x = t; loads the memory location x with the
value of expression t’.

1.3.2 Decomposition of the State

A state s is a function that maps a finite subset of Var to the set Val. It will be
helpful for the next chapter if we decompose this function as the composition
of two other functions of finite domains: the first is known as the environment,
which maps a finite subset of the set Var to an intermediate set Ref, whose
elements are called references and the second, is called the memory state, which
maps a finite subset of the set Ref to the set Val.
Var Ref Val

e m

This brings us to propose two infinite sets, Var and Ref, and a set Val of
values. The set of environments is defined as the set of functions that map a
finite subset of the set Var to the set Ref. The set of memory states is defined as
the set of functions mapping a finite subset of the set Ref to the set Val. For the
set of environments, we define an update function + such that the environment
e + (x = r) is identical to e, except at x, which now becomes associated with
10 1. Imperative Core

the reference r. For the set of memory states, we define an update function +
such that the memory state m + (r = v) is identical to m, except at r, which
now becomes associated with the value v.
However, constant variables complicate things a little bit. For one, the envi-
ronment must keep track of which variables are constant and which are mutable.
So, we define an environment to be a function mapping a finite subset of the
set Var to the set {constant, mutable} × Ref. We will, however, continue
to write e(x) to mean the reference associated to x in the environment e.
Then, at the point of execution of the declaration of a constant variable
x, we directly associate the variable to a value in the environment, instead of
associating it to a reference which is then associated to a value in the mem-
ory state. The idea is that the memory state contains information that can be
modified by an assignment, while the environment contains information that
cannot. To avoid having a target set for the environment function that is overly
complicated, we propose that Ref is a subset of Val, which brings us to pro-
pose that the environment is a function that maps a finite subset of Var to
{constant, mutable} × Val and the memory state is a function that maps
a finite subset of Ref to Val.
Var Val

Ref

1.3.3 A Visual Representation of a State

It can be helpful to visualise states with a diagram. Each reference is represented


with a box. Two boxes placed in different positions always refer to separate
references.

Then, we represent the environment by adding one or more labels to certain


references.
1.3 The Semantics of the Imperative Core 11

a x b

Even though each label is associated with a unique reference, nothing prevents
two labels from being associated with the same reference, since an environment
is a function, but not necessarily an injective function. Finally, we represent
the memory state by filling each square with a value.

a x b

4 5

When a variable is associated directly with a value in the environment, we


do not draw a box and we put the label directly on the value.

1.3.4 The Value of Expressions

The function Θ now associates a value to each triplet composed of an expres-


sion, an environment, and a memory state. For example, Θ(x + 3,[x = r1 ,
y = r2 ],[r1 = 5, r2 = 6]) = 8.
For Java, this function is then defined as
– Θ(x,e,m) = m(e(x)), if x is a mutable variable in e,
– Θ(x,e,m) = e(x), if x is a constant variable in e,
– Θ(c,e,m) = c, if c is a constant, such as 4, true, etc.,
– Θ(t + u,e,m) = Θ(t,e,m) + Θ(u,e,m),
– Θ(t - u,e,m) = Θ(t,e,m) - Θ(u,e,m),
12 1. Imperative Core

– Θ(t * u,e,m) = Θ(t,e,m) * Θ(u,e,m),


– Θ(t / u,e,m) = Θ(t,e,m) / Θ(u,e,m),
– Θ(t % u,e,m) = Θ(t,e,m) % Θ(u,e,m),
– if Θ(b,e,m) = true then

Θ((b) ? t : u,e,m) = Θ(t,e,m),

if Θ(b,e,m) = false then

Θ((b) ? t : u,e,m) = Θ(u,e,m).

At first glance, this definition may seem circular, since to define the value
of an expression of the form t + u, we use the value of expressions t and u.
But the size of these expressions is smaller than that of t + u. This definition
is therefore a definition by induction on the size of expressions.
The first clause of this definition indicates that the value of an expression
that is a mutable variable is m(e(x)). We apply the function e to the variable x,
which produces a reference, and the function m to this reference, which produces
a value. If the variable is a constant variable, on the other hand, we find its
value directly in the environment.
The definition of the function Θ for Caml is identical, except in the case of
variables, where we have the unique clause
– Θ(x,e,m) = e(x),
where the variable x is either mutable or constant.
For example, if e is the environment [x = r] and m is the memory state
[r = 4] and that the variable x is mutable in e, the value Θ(x,e,m) is 4 in
Java, but is r in Caml.
Caml also has a construct ! such that
– Θ(!t,e,m) = m(Θ(t,e,m)).
If x is a variable, then the value of !x is Θ(!x,e,m) = m(Θ(x,e,m)) =
m(e(x)) that is the value of x in Java. This explains why we write y := !x +
1 in Caml, where we write y = x + 1; in Java.
In Caml, references that can be associated to an integer in memory are of
the type int ref. For example, the variable x and the value r from this example
are of the type int ref. In contrast to the variable x, the expressions !x, !x +
1, ... are of the type int.
The definition of the function Θ for C is the same as the definition used for
Java.
1.3 The Semantics of the Imperative Core 13

Exercise 1.4
Give the definition of the function Θ for expressions of the form t & u
and t | u.
Unlike the boolean operator & that evaluates its two arguments, the
operator && evaluates its second argument only if the first argument
evaluates to true. Give the definition of the function Θ for expressions
of the form t && u.
Answer the same question for the boolean operator ||, which only eval-
uates its second argument if the first argument evaluates to false.

1.3.5 Execution of Statements

The function Σ now associates memory states to triplets composed of an in-


struction, an environment, and a memory state. The function Σ in Java is
defined below.
– When the statement p is a mutable variable declaration of the form {T x =
t; q}, the function Σ is defined as follows

Σ({T x = t; q},e,m) = Σ(q,e + (x = r),m + (r = Θ(t,e,m)))

where r is a new reference that does not appear in e or m.


– When the statement p is a constant variable declaration of the form {final
T x = t; q}, the function Σ is defined as follows

Σ({final T x = t; q},e,m) = Σ(q,e + (x = Θ(t,e,m)),m).

– When the statement p is an assignment of the form x = t;, the function is


defined as follows

Σ(x = t;,e,m) = m + (e(x) = Θ(t,e,m)).

– When the statement p is a sequence of the form {p1 p2 }, the function Σ is


defined as follows

Σ({p1 p2 },e,m) = Σ(p2 ,e,Σ(p1 ,e,m)).

– When the statement p is a test of the form if (b) p1 else p2 , the function
Σ is defined as follows. If Θ(b,e,m) = true then
14 1. Imperative Core

Σ(if (b) p1 else p2 ,e,m) = Σ(p1 ,e,m).

If Θ(b,e,m) = false then

Σ(if (b) p1 else p2 ,e,m) = Σ(p2 ,e,m).

– This brings us to the case where the statement p is a loop of the form while
(b) q. We have seen that introducing the imaginary statement skip; such
that Σ(skip;,e,m) = m, we can define the statement while (b) q as a
shorthand for the infinite statement

if (b) {q if (b) {q if (b) {q if (b) ...


else skip;}
else skip;}
else skip;}
else skip;

When dealing with these types of infinite constructs, we often try to ap-
proach them as limits of finite approximations. We therefore introduce an
imaginary statement called giveup; such that the function Σ is never de-
fined on (giveup;,e,m). We can define a sequence of finite approximations
of the statement while (b) q.
p0 = if (b) giveup; else skip;
p1 = if (b) {q if (b) giveup; else skip;} else skip;
...
pn+1 = if (b) {q pn } else skip;.
The statement pn tries to execute the statement while (b) q by completing
a maximum of n complete trips through the loop. If, after n loops, it has not
terminated on its own, it gives up.
If isn’t hard to prove that for every integer n and state e, m, if Σ(pn ,e,m)
is defined, then for all n’ greater than n, Σ(pn ,e,m) is also defined, and
Σ(pn ,e,m) = Σ(pn ,e,m). This formalises the fact that if the statement
while (b) q terminates when the maximum number of loops is n, then it
also terminates, and to the same state, when the maximum number of loops
is n’.
There are therefore two possibilities for the sequence Σ(pn ,e,m): either it is
never defined, or it is defined beyond a certain point, and in this case, it is
constant over its domain. In the second case, we call the value it takes over
its domain the limit of the sequence. In contrast, the sequence does not have
1.3 The Semantics of the Imperative Core 15

a limit if it is never defined. We can now define the function Σ in the case
where the statement p is of the form while (b) q

Σ(while (b) q,e,m) = limn Σ(pn ,e,m).

Note that the statements pi are not always shorter than p, but if p contains
k nested while loops, pi contains k - 1. The definition of the function Σ is
thus a double induction on the number of nested while loops, and on the size
of the statement.
Exercise 1.5
What is the memory state Σ(x = 7;,[x = r],[r = 5])?
The definition of the function Σ for Caml is not very different from the
definition used for Java. In Caml, any expression that evaluates to a reference
can be placed to the left of the sign :=, while in Java, only a variable can appear
to the left of the sign =. The value of the function Σ of Caml for the statement
t := u is defined below:
– Σ(t := u,e,m) = m + (Θ(t,e,m) = Θ(u,e,m))
In the case where the expression t is a variable x, we have Σ(x := u,e,m)
= m + (Θ(x,e,m) = Θ(u,e,m)) = m + (e(x) = Θ(u,e,m)) and we end up
with the same definition of Σ used for Java.
The definition of the function Σ for C is not very different from the defini-
tion used for Java. The main difference is in case of variable declaration
Σ({T x = t; q},e,m) = (Σ(q,e+(x=r),m + (r = Θ(t,e,m))))|Ref−{r}
where r is a new reference that does not appear in e or m, and the notation
m|Ref−{r} designates the memory state m in which we have removed the ordered
pair r = v if it existed. Thus, if we execute the statement {int x = 4; p} q
in the state e, m, we execute the statement p in the state e + (x = r), m +
(r = 4) in C as in Java. In contrast, we execute the statement q in the state
e, m + (r = 4) in Java and in the state e, m in C.
As, in the environment e, there is no variable that allows the reference r
to be accessed, the ordered pair r = 4 no longer serves a purpose sitting in
memory. Thus, whether it is is left alone, as in Java or Caml, or deleted, as
in C, is immaterial. However, we will see, in Exercise 2.17, that this choice in
C is a source of difficulty when the language contains other constructs.
Exercise 1.6
The incomplete test allows the creation of a statement composed of a
boolean expression and a statement. This statement is written if (b)
p. The value of the function Σ for this statement is defined as follows. If
Θ(b,e,m) = true then
16 1. Imperative Core

Σ(if (b) p,e,m) = Σ(p,e,m).

If Θ(b,e,m) = false then

Σ(if (b) p,e,m) = m.

Show that it is possible to define this construct using a complete test


and the statement skip;.
Exercise 1.7
The loop do allows the creation of a statement composed of a boolean
expression and a statement. This statement is written do p while (b).
This is a shorthand of the statement {p while (b) p}. Give the defini-
tion of the function Σ for this construct.
Exercise 1.8
The loop for allows the creation of a statement composed of three state-
ments and a boolean expression. This statement is written for(p1 ; b;
p2 ) p3 . It is a shorthand for the statement p1 ; while (b) {p3 p2 ;}.
What does the following statement do?

{y = 1; for(x = 1; x <= 10; x = x + 1) y = y * x;}

Exercise 1.9
Give the definition of the Σ function for the declaration of a variable
without an initial value.
Exercise 1.10
Imagine an environment e — which cannot be created in Java — [x =
r, y = r], m, the memory state [r = 4], p, the statement x = x + 1;,
and m’, the memory Σ(p,e,m). What is the value associated with y in
the state e, m’? Answer the same question for the environment [x =
r1 , y = r2 ] and memory [r1 = 4, r2 = 4].
Draw these two states.
Exercise 1.11
Imagine that all memory states have a special reference: out. Define the
function Σ for the output construct System.out.print from the Section
1.2.
Exercise 1.12
In this exercise, imagine a data type that allows integers to be of any
size. To each statement p in the imperative core of Java, we associate the
1.3 The Semantics of the Imperative Core 17

partial function from integers to integers that, to the integer n, associates


the value associated to out in the memory state Σ(p,[x = in, y =
out],[in = n, out = 0]).
A partial function f, from integers to integers, is called computable if
there exists a statement p such that f is the function associated with p.
Show that there exists a function that is non computable.
Hint: use the fact that there does not exist a surjective function of N in
the set of functions from N to N.

You might also like