Using Zoom for Lectures
• Please mute both:
• yourvideocamerasfortheentirelecture
• youraudio/micsunlessaskingoransweringaquestion
• Recommended Zoom configuration:
• notfullscreen(double-clickanywheretoexitfullscreen)
• side-by-side mode (see View options near the top of Zoom)
• Asking/answering a question, option 1:
• clickonParticipants
• usethehandicontoraiseyourhand
• Iwillcallonyouandaskyoutounmuteyourself
• Asking/answering a question, option 2:
• clickonChat
• typeyourquestion,andIwillanswerit
CS 320 : Operational Semantics Scope
Marco Gaboardi MSC 116 gaboardi@bu.edu
Announcements
Programming Assignment #4 is due on Friday, April 3.
Grading Policy for Spring 2020: Read the article in BU Today,
University to Offer Students Credit/No Credit Option
Programming Assignment #5 will be posted on Friday, April 3.
TopHat questions are included in Zoom meetings, but not graded.
All Zoom meetings are recorded (by default), and their recordings available for download shortly after the live meetings.
All Zoom links for CS 320 are at the bottom of the Resources webpage on Piazza.
Learning Goals for today
• Tounderstandhowthedynamicsemanticsofaprogram
describes the meaning of a program.
• Tounderstandthesubtletiesofdifferentevaluation
strategies.
• Diggingintotheconceptsofbindingandscope.
Arithmetical expressions: shape of expressions • Let us consider this simple language for expressions
Adtkw.e.-1-i’l’..Q.l .e,i
{
(val>
£)(,:,,-r[H ,,+ar;.\–l,\\lt-te.til.,._\ N, sV’l{ M Q. :
e,)
, …….
a.dd
I•-
. . –
.,. •••
.- C’ .. –
,
a.Jd. 5 J yt,t£vtl-l.S (::, J &dJ ( WUIW-S 1) ‘) ( ( ( X aJi.l 5 ) WU:VU-6 Y) ar.U ({i WUws L))
( {_ C 3
Operational semantics for arithmetical expressions
(e/m) → (e/m)
Here (e/m) is a configuration where e is an expression and
m is a memory.
We can think about a memory as a set of (unique)
assignments of variables to values:
m =((x1=v1),(x2=v2)…,(xn=vn))
The memory is the environment where the variable of an expression are defined.
Arithmetical expressions: shape of expressions • Let us consider this simple language for expressions
• What is the potential shape of an expression?
•v
•x
• e add (n|x)
Value
Variable
Expression + Constant or Variable
This is recursive
Summary of the rules:
(F) (x/m) → (fetch(x,m)/m)
(+A)(e add x/m) → (e add fetch(x,m)/m)
(+B)(x add v/m) → (fetch(x,m) add v/m) (+C)(v1 add v2/m) → (v1+v2/m)
(e/m) → (e1/m)
(e add v2/m) → (e1 add v2/m)
(+D)
Summary of the rules:
(-A)(e minus x/m)→(e minus fetch(x,m)/m) (-B)(x minus v/m)→(fetch(x,m) minus v/m)
(-C)(v1 minus v2/m) → (v1-v2/m)
(e/m) → (e1/m)
(e minus v2/m) →(e1 minus v2/m)
(-D)
EV ‘~ ‘c.rvi of(((::>add S)·minu> ~}add ( WIinu>1))
Y’ fuAM~()-
0 €- e ~ } P – ~ m , , F – t W – P-w~ ~6Wll~r/J A-l-o~ ·. ·
(( ( 3 a,d,J s) Vv’Vil’IU$ 6) o.old {o{ ‘fVl(vw.> 1))-> ( ( 8 YlitiVU,t,S b ) o..dJ ( YIMvtMA 1)) · >
( (2 A-dJ. (/2 mivws f)J ( d. advd. 1 )
f Bi {.{_(Xadd5)rw,i.uw Y)add {:J. ri<,'= Z)) t,,-tL_ ex=3, y= z=1) vY1,
a'tJCUM w– (C(Jadtls-)1%l’VWA b) ru1J.C-Jvw:VU-0z)Iwi
( ( ( 3 aJd1 5) WILVU<4 6) a_dd; ( ;;z Vvt,ivu,tS 1)/ 1tv1 •
TopHat Q1 - Q3
Variables
Variables
• Functional languages use variables as names (where the
association name-value is stored in an environment).
• We can remember the association, or read the value, but
we cannot change it.
• Imperative languages are abstractions of von Neumann architecture
• A variable abstracts the concept of memory location
• Understanding how variables are managed is an important part to understand the semantics of a programming language.
11
Let in a Functional Language
Let expression
• Let us consider this simple language for expressions
• What is the semantics of a let expression?
Another Example
subsDtute 2 for x
29
let x = 2 in
let y = x + x in y*x
Moral: Let operates by subs&tu&ng computed values for variables
let y = 2 + 2 in y*2
–>
–>
subsDtute 4 for y
let y = 4 in y*2
4*2
8
–> –>
Rules for let
(e1/m) → (e3/m)
(let x=e in e /m) →(let x=e in e /m) 1 2 ?? 3 2
We can use the fact that e1 is recursive and hypothetical reasoning.
Recording the value of a variable
(let x=v in e/m) →
If variables are just names for values, where shell we store
the name-value association?
This is the role of the environment, storing name-value associations.
??
(e/m@(x=v))
((x1=v1),(x2=v2)…,(xn=vn))
Where we use the symbol @ to extend the environment with a new name-value association.
What happens if m already contains u?
Extending an environment
Suppose that we have
m=((x=1),(z=5),(y=3))
Then, if we extend m with the new pair (u=4), in symbols
m@(u=4) m@(u=4)=((x=1),(z=5),(y=3),(u=4))
We get:
Summary of the rules:
(F) (x/m) → (fetch(x,m)/m)
(A)(e add x/m) → (e add fetch(x,m)/m)
(B)(x add v/m) → (fetch(x,m) add v/m) (C)(v1 add v2/m) → (v1+v2/m)
(D) (T) (L)
(e/m) → (e1/m)
(e add v2/m) → (e1 add v2/m)
(e1/m) → (e3/m)
(let x=e1 in e2/m) →(let x=e3 in e2/m)
(let x=v in e/m) → (e/m@(x=v))
Example:
Let us call m=(x=3,y=5,z=6) we have:
(x add y/m) → (x add 5/m) ———————————————————
(let k=(x add y)in(k add z)/m) →(let k=(x add 5)in(k add z)/m)
(x add 5/m) → (3 add 5/m) ———————————————————
(let k=(x add 5)in(k add z)/m)→(let k=(3 add 5)in(k add z)/m) =
(3 add 5/m) → (8/m) —————————————————– (let k=(3 add 5)in(k add z)/m)→(let k=8 in(k add z)/m) →
(k add z/m@(k=8))→(k add 6/m@(k=8))→(8 add 6/m@(k=8)) →(14/m@(k=8))
=
TopHat Q4 – Q6
Update in a Imperative Language
Assignment
• Let us consider this simple language for expressions
• What is the semantics of an assignment?
Operational semantics for programs with assignments
(prog/m) → (prog/m)
Here (prog/m) is a configuration where prog is a program
and m is a memory.
We can think about a memory as a set of (unique)
assignments of variables to values:
m =((x1=v1),(x2=v2)…,(xn=vn))
The memory is the environment where the variable of an expression are defined.
Rules for assignment
(e1/m) → (e2/m)
(x:=e;prog/m) →(x:=e;prog/m)
1
??
2
We can use thypothetical reasoning.
An example: recording the value of a variable
(x:=v;prog/m) →(prog/update(x,v,m)) ??
Where we use the function update(x,v,m) to update the value of the variable x in m to v.
What happens if m does not contain x?
Updating an environment
Suppose that we have
m=((x=1),(z=5),(y=3))
Then, if we update m with the following command
update(x,4,m) update(x,4,m)=((x=4),(z=5),(y=3))
We get:
Initializing a variable
Suppose that we have
m=((u=1),(z=5),(y=3))
What shall we do if we have the following?
update(x,4,m)
Basically there are two strategies: 1- we create a new pair:
update(x,4,m)=((u=1),(z=5),(y=3),(x=4))
2- we give an error because the variable has not been initialized – how can we fix this?
Example:
Let us call m=(x=3,y=5,z=6,u=0) we have:
(x add 5/m) → (3 add 5/m)
—————————
(z:=x add 5 ; u:=u add z;p/m) →(z:=3 add 5 ; u:=u add z;p/m) =
(3 add 5/m) → (8/m) ——————————————————— (z:=3 add 5 ; u:=u add z;p/m)→(z:=8; u:=u add z;p/m) =
m’=(x=3,y=5,z=8,u=0)
—————————————————– (z:=8; u:=u add z;p/m)→(u:=u add z;p /m’) =
(u add z/m’) → (u add 8/m’) ————————————— (u:=u add z;p/m’)→(u:=u add 8;p/m’) =
Example:
(u add 8/m’) → (0 add 8/m’) ————————————— (u:=u add 8;p/m’)→(u:=0 add 8;p/m’) =
(0 add 8/m’) → (8/m’) ————————————— (u:=0 add 8;p/m’)→(u:=8;p/m’) =
m’’=(x=3,y=5,z=8,u=8)
—————————————————– (u:=8;p/m)→(p/m’’) → …
TopHat Q7 – Q9
Mutable vs Immutable Variables
• When we consider variables as names we are working with
immutable variables (e.g. the part of OCaml we studied)
• When we consider variables as memory locations we are working with mutable variables (e.g. Python, c, etc.)
• Understanding how variables are managed is an important part to understand the semantics of a programming language.
32
Mapping the formal semantics to an implementation
• Our formal rules for the interpreter language operated over “configurations” that contained the program (list of commands) and a stack (list of values with type tags)
• Consequence: lets write a function that operates over a list of commands and a stack
let rec foo commandList stack =
match (commandList, stack) with
| (Add::cs, I(x)::I(y)::s) -> foo cs I(x+y)::s
(p/S) → (p’/S’)
(B) (add;p/int(v2)::int(v1)::S) → (p/int(v2+v1)::S)
Mapping the formal semantics to an implementation
• Our formal rules for the interpreter language operated over “configurations” that contained the program (list of commands) and a stack (list of values with type tags)
• Consequence: lets write a function that operates over a list of commands and a stack
let rec foo commandList stack =
match (commandList, stack) with
| (Add::cs, I(x)::I(y)::s) -> foo cs I(x+y)::s
| (Div::cs, I(x)::I(0)::s) -> foo cs E::I(x)::I(0)::s | (Div::cs, I(x)::I(y)::s) -> foo cs I(x/y)::s
(div;p/int(v2)::int(0)::S)→(p/(:error:)::int(v2)::int(0)::S
v1≠0
What about this?
(div;p/int(v2)::int(v1)::S) → (p/int(v2/v1)::S)
)
Mapping the formal semantics to an implementation
• Our formal rules for the interpreter language operated over “configurations” that contained the program (list of commands) and a stack (list of values with type tags)
• Consequence: lets write a function that operates over a list of commands and a stack
let rec foo commandList stack =
match (commandList, stack) with
| (Add::cs, I(x)::I(y)::s) -> foo cs I(x+y)::s | (Div::cs, I(x)::I(0)::s) -> foo cs E::stack | (Div::cs, I(x)::I(y)::s) -> foo cs I(x/y)::s
Can also write it this ways
(div;p/int(v2)::int(0)::S)→(p/(:error:)::int(v2)::int(0)::S
v1≠0
(div;p/int(v2)::int(v1)::S) → (p/int(v2/v1)::S)
)
Operational semantics for the interpreter
(p/S) → (p’/S’)
Here (p/S) is a configuration where p is a program and S is a stack. We call these pairs configurations because we think in terms of an “abstract machine”.
We can think about the stack as a list of values (denoted with v):
vn::…::v2::v1::[]
We say that from the configuration (p/S) we can step (or reduce) to the configuration (p’/S’) in one step.
Operational semantics for arithmetical expressions
(e/m) → (e/m)
Here (e/m) is a configuration where e is an expression and m is an environment. We call these pairs configurations because we think in terms of an “abstract machine”.
We can think about an environment as a set of (unique) assignments of variables to values:
m =((x1=v1),(x2=v2)…,(xn=vn))
Tips for interpreter part2:
Operational semantics for the interpreter with variables
(p/S,m) → (p’/S’,m’)
Here (p/S,m) is a configuration where p is a program and
S is a stack, and m is an environment.
We can think about the stack as a list of values:
vn::…::v2::v1::[]
We can think about an environment as a set of (unique) assignments of variables to values:
m =((x1=v1),(x2=v2)…,(xn=vn))
Tip for interpreter part2: Implementation of OCaml let
We could imagine the let construction we saw in OCaml and in the last class:
let x=v in …
to be implemented as
pushI v
pushN x
bind
…
Scoping rules
Variable names
How shall we evaluate this expression?
Is it referring to this definition?
let k=3 in (let k=2 in k+5)
Is it referring to this definition?
What is the value of k here?
Scope of a variable
• The scope of a variable is the range of statements over
which it is visible
• The scope rules of a language determine how references to names are associated with variables
let k=3 in (let k=2 in k+5)
OCaml scoping rule says that a variable name is statically associated with the closest definition in the abstract syntax tree.
Back to our example
This is the first declaration we find
Start from here
let k=3 in (let k=2 in k+5)
To find the value of k we look search declarations, first locally, then in increasingly larger enclosing scopes
Another example
This is the first declaration we find
Start from here
let k=3 in (let z=2 in k+5)
To find the value of k we look search declarations, first locally, then in increasingly larger enclosing scopes
Another example
This is the first declaration we find
Start from here
let k=3 in k + (let k=2 in k+5)
This is the first declaration we find
Start from here
Another example
This is the first declaration we find
Start from here
let k=3 in (let k=2 in k+5) + k
This is the first declaration we find
Start from here
Static Scope
• Based on program text
• To connect a name reference to a variable, we (or the compiler) must find the declaration
• Some languages allow nested subprogram definitions, which create nested static scopes
• Search process:
search declarations, first locally, then in increasingly larger enclosing scopes, until one is found for the given name
Static Scope
• Variables can be hidden from a unit by having a “closer”
variable with the same name
declaration of x
declaration of x use of x
Static Scope
• Variables can be hidden from a unit by having a “closer”
variable with the same name
declaration of x
declaration of x use of x
use of x
Static Scope
• Search process:
search declarations, first locally, then in increasingly larger enclosing scopes, until one is found for the given name
• Enclosing static scopes (to a specific scope) are called its static ancestors; the nearest static ancestor is called a static parent
TopHat Q10 – Q12
Scope Blocks
A method of creating static scopes inside program units (ALGOL 60)
void sub() {
int count;
while (…) {
int count;
count++; …
} …
}
Program constructs (“blocks”) create scopes
Scope Block Example:
int main()
{
int x=5;
{
int x=4;
printf(“The value of x in the block is %d\n”, x);
}
printf(“The value of x in outside the block is %d”,
x);
return 0; }
In C we can write a program like the one above
Scope Block Example:
int main()
{
int x=5;
{
int x=4;
printf(“The value of x in the block is %d\n”, x);
}
printf(“The value of x in outside the block is %d”,
x);
return 0; }
Tip for interpreter part2: let…end construction
In the interpreter description for part 2 we require to implement a construction
let … end this is like a scope block { … }.