程序代写代做代考 ocaml interpreter C compiler Using Zoom for Lectures

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
::= | ::= add | minus
::= var | val

Adtkw.e.-1-i’l’..Q.l .e,iJ3, 4,R,ofle.f-..,re..if:


{
(val>
£)(,:,,-r[H ,,+ar;.\–l,\\lt-te.til.,._\ N, sV’l{ M Q. :
e,);-\-k,;>
, …….
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
::= | ::= add
::= var | val
• 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 ::= let var= in |
|
::= add ::= var | val
• 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 ::= | ; ::= var :=
::= |
::= add
::= var | val
• 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 { … }.