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
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.
Equifax agreed in paying between 570 and 700 million dollars settlement
What kind of bug?
Vulnerability in the exception handling of parsing in Apache Struts open software
Interesting and entertaining reading
If you want to know more about Apache Struts 2 and Equifax: Apache Struts 2 is an open-source web application framework for
developing Java EE web applications.
Equifax Inc. is one of the three largest consumer credit reporting agencies, along with Experian and TransUnion. Equifax collects and aggregates information on over 800 million individual consumers and more than 88 million businesses worldwide.
If you want to know more about the software security bug in Struts 2, which was later exploited in a massive data breach by Equifax:
“Equifax couldn’t find or patch vulnerable Struts implementations”, The Register, October 2, 2017.
“A series of delays and major errors led to massive Equifax breach”, Ars Technica, October 2, 2017.
Another security breach caused by malfunctioning software:
Zoombombing (if you have not heard or read about it, search for articles on the Web – many have been published since mid-March).
Is it a bug or a feature in the Zoom software? We are still waiting for a final judgment on this …
Are type error dangerous?
Learning Goals for today
• Tounderstandhowthedynamicsemanticsofaprogram
describes the meaning of a program.
• Tounderstandthesubtletiesofdifferentevaluation
strategies.
• Diggingintotheconceptsofbindingandscope.
Language for the Interpreter (simplified)
The language for the interpreter can be described by the following
grammar:
We use ; here
to separate
commands, in
| neg | rem | swap
the
interpreter we
use a newline.
• A program is a sequence of commands followed by quit.
• A command is one the keywords above – in the case of push this is
followed by a constant.
• A (simplified) constant is either an int or a string.
• We will denote arbitrary programs with p,p’,…
Multiple steps of Operational semantics
We have seen the reduction relation between configurations:
We say that from the configuration (p, S) we can step (or reduce) to the configuration (p’,S’) in one step.
In general we are interested in (finite or infinite) sequences of reduction steps:
(p,S) → (p’,S’)
(p1,S1) → (p2,S2) → (p3,S3) →… → (pk,Sk)
Summary of some rules:
(A) (push num;p/S) → (p/num::S)
(B) (add;p/int(v2)::int(v1)::S) → (p/int(v2+v1)::S)
(C) (add;p/type(v1)::[]) → (p/(:error:)::type(v1)::[]) (D) (add;p\[]) → (p\(:error:)::[])
(E) (quit/S) → print(S)
(F) (add;p/notint(v)::S)→(p/(:error:)::notint(v)::S)
(G) (add;p/int(v1)::notint(v2)::S) →(p/(:error:)::int(v1)::notint(v2)::S)
Let’s give to each rule a name.
An example:
(push 5;push 4;add;quit/S) →
(A) (push 4;add;quit/int(5)::S) → (A) (add;quit/int(4)::int(5)::S) → (B) (quit/int(4+5)::S) →
(E) print(int(4+5)::S)
Another example:
(push 5;add;quit/[]) →
(A) (add;quit/int(5)::[]) →
(C) (quit/(:error:)::int(5)::S) → (E) print((:error:)::int(5)::S)
TopHat Q1 – Q5
Another example: div
Informal description: The command div refers to integer division. It is a binary operator and works in the following way:
• if top two elements in the stack are integer numbers, pop the top element(y) and the nextelement(x), divide x by y, and push the result x back onto the stack y
• if top two elements in the stack are integer numbers but y equals to 0, push them back in the same order and push :error: onto the stack
• if the top two elements in the stack are not all integer numbers, push them back in the same order and push :error: onto the stack
• if there is only one element in the stack, push it back and push :error: onto the stack
• if the stack is empty, push :error: onto the stack
Another example: div Formal description:
(div;p/int(v2)::int(v1)::S) → (p/int(v2/v1)::S) (div;p/type(v1)::[]) → (p/(:error:)::type(v1)::[]) (div;p\[]) → (p\(:error:)::[])
(div;p/notint(v)::S)→(p/(:error:)::notint(v)::S) (div;p/int(v1)::notint(v2)::S)
→(p/(:error:)::int(v1)::notint(v2)::S)
Are we done?
Informal description:
if top two elements in the stack are integer numbers but y equals to 0, push them back in the same order and push :error: onto the stack
Another example: div Formal description:
(div;p/int(v2)::int(v1)::S) → (p/int(v2/v1)::S) (div;p/type(v1)::[]) → (p/(:error:)::type(v1)::[]) (div;p\[]) → (p\(:error:)::[])
(div;p/notint(v)::S)→(p/(:error:)::notint(v)::S) (div;p/int(v1)::notint(v2)::S)
→(p/(:error:)::int(v1)::notint(v2)::S)
(div;p/int(v2)::int(0)::S)
→ (p/(:error:)::int(v2)::int(0)::S)
What is the problem?
Another example: div If we have the configuration:
(div;p/int(2)::int(0)::S) We can apply either one of the following rules
(div;p/int(v2)::int(v1)::S) → (p/int(v2/v1)::S) (div;p/int(v2)::int(0)::S)
This is not defined! That is why we want another rule!
→ (p/(:error:)::int(v2)::int(0)::S) (div;p/int(2)::int(0)::S) → (p/int(2/0)::S)
(div;p/int(2)::int(0)::S)
→ (p/(:error:)::int(2)::int(0)::S)
And obtain:
Rules with hypothesis
We want some way to express a condition under which we can apply a rule.
One way to do this is by adding an hypothesis:
(p/S) satisfies the
hypothesis
(p/S) → (p’/S’)
Example:
v1≠0 (div;p/int(v2)::int(v1)::S)→(p/int(v2/v1)::S)
Another example: div Formal description:
v1≠0
(div;p/int(v2)::int(v1)::S) → (p/int(v2/v1)::S) (div;p/type(v1)::[]) → (p/(:error:)::type(v1)::[]) (div;p\[]) → (p\(:error:)::[])
(div;p/notint(v)::S)→(p/(:error:)::notint(v)::S) (div;p/int(v1)::notint(v2)::S)
→(p/(:error:)::int(v1)::notint(v2)::S) (div;p/int(v2)::int(0)::S)→(p/(:error:)::int(v2)::int(0)::S)
We will leave implicit the lines of the rule with no hypothesis.
Language for the Interpreter (simplified)
The language for the interpreter can be described by the following grammar:
| neg | rem | swap
What is the form of a program?
Is this the common way we write programs?
Arithmetical expressions: shape of expressions • Let us consider this simple language for expressions
What are the challenges here?
What is the form of a program?
[[
Do we need a stack here?
Arithmetical expressions: shape of expressions • Let us consider this simple language for expressions
What are the challenges here?
What is the value of a var?
X add 5 add 6
Where is the value defined?
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 call these pairs configurations because we think in terms of an “abstract machine”.
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
An example: addition of values
What can we do when we have an expression instead of a value v1?
(v1 add v2/m) → (v1+v2/m)
Here we use v1+v2 to actually mean the result of summing the two values
An example: addition of values
(e/m) → (e1/m)
(e add v2/m) → (?e?1 add v2/m)
We can use the fact that e is recursive and hypothetical reasoning.
An example: fetching the value of a variable
(x/m) → ?(f?etch(x,m)/m) How can we fetch the value of x from the environment?
We can introduce a function fetch taking an environment a variable and returning the value of the variable in the environment.
fetch(x2,((x1=v1),(x2=v2)…,(xn=vn))=v2
An example: fetching the value of a variable
The variable can appear in an expression. On the right:
(e add x/m) → (e add fetch(x,m)/m)
Or on the left:
(x add v/m) → (fetch(x,m) add v/m)
How about a value?
(n/m) → ??
What does a number evaluate to?
This is a value, so we don’t have any step
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)
An example:
(3 add 5/()) → (8/()) ————————————
(3 add 5 minus 6/())→ (8 minus 6/())→ (2/())
How many steps of reduction?
Another example:
Let us call m=(x=3,y=5,z=6) we have: (x add y minus z/m) →
(x add y/m) → (x add 5/m) ————————————— (x add y minus 6/m)→(x add 5 minus 6/m) =
(x add 5/m) → (3 add 5/m) ————————————— (x add 5 minus 6/m)→(3 add 5 minus 6/m) =
(3 add 5/m) → (8/m) ———————————
(3 add 5 minus 6/m)→(8 minus 6/m) → (2/m)
Yet another example:
Let us call m=(x=3,y=5,z=6) we have: (x add 4 minus z/m) →
(x add 4/m) → (3 add 4/m) ————————————
(x add 4 minus 6/m)→(3 add 4 minus 6/m) =
(3 add 4/m) → (8/m) ———————————
(3 add 4 minus 6/m)→(7 minus 6/m) → (1/m)
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.
40
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.
An example: 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.
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 minus z/m)→(let k=x add 5 in k minus z/m) =
(x add 5/m) → (3 add 5/m) ———————————————————
(let k=x add 5 in k minus z/m)→(let k=3 add 5 in k minus z/m) =
(3 add 5/m) → (8/m) —————————————————– (let k=3 add 5 in k minus z/m)→(let k=8 in k minus z/m) →
(x add y/m) → (x add 5/m) —————————————
(k minus z/m@(k=8))→(k minus 6/m@(k=8))→(8 minus 6/m@(k=8))
→(2/m@(k=8))
TopHat Q6 – Q12