南京大学：《程序设计语言的形式语义》课程教学资源（课件讲稿）01_Introduction（主讲：冯新宇）Formal Semantics of Programming Languages

Formal Semantics of Prog.Lang. -ntroduction Xinyu Feng(冯新宇) Nanjing University Acknowledgments:some slides are taken from Zhong Shao's slides for Yale Formal Semantics class

Formal Semantics of Prog. Lang. – Introduction Xinyu Feng (冯新宇) Nanjing University Acknowledgments: some slides are taken from Zhong Shao’s slides for Yale Formal Semantics class

Programming Languages A fundamental field in computer science -As classic as OS and Architectures ·SOSP:1967;ISCA:1973;POPL:1973 Old,but still very active Many important research problems New languages keep showing up Rust,Go,Scala,F#,R,Matlab,tensorflow,P4,.. Formal Semantics of Prog.Lang. 09/07/2018

Programming Languages • A fundamental field in computer science – As classic as OS and Architectures • SOSP: 1967；ISCA: 1973；POPL: 1973 • Old, but still very active – Many important research problems – New languages keep showing up • Rust, Go, Scala, F#, R, Matlab, tensorflow, P4, … Formal Semantics of Prog. Lang. 09/07/2018

Programming Languages Computer Science is no more about computers than astronomy is about telescopes. Edsger W.Dijkstra How about PL then? Formal Semantics of Prog.Lang. 09/07/2018

Programming Languages Formal Semantics of Prog. Lang. 09/07/2018 Computer Science is no more about computers than astronomy is about telescopes. Edsger W. Dijkstra How about PL then?

Programming Languages PL research is broader than designing and implementing new languages.To me,a PL researcher is someone who views the programming language as having a central place in solving computing problems.From this vantage point,PL researchers tend to focus on developing general abstractions,or building blocks,for solving problems,or classes of problems.PL research also considers software behavior in a rigorous and general way, e.g.,to prove that (classes of)programs enjoy properties we want,and/or eschew properties we don't.This approach has proven to be very valuable for solving a wide ranging set of problems. Mike Hick's blog post: What is PL research and how is it useful?-The PL Enthusiast www.pl-enthusiast.net/2015/05/27/what-is-pl-research-and-how-is-it-useful/

Programming Languages What is PL research and how is it useful? - The PL Enthusiast Mike Hick’s blog post: PL research is broader than designing and implementing new languages. To me, a PL researcher is someone who views the programming language as having a central place in solving computing problems. From this vantage point, PL researchers tend to focus on developing general abstractions, or building blocks, for solving problems, or classes of problems. PL research also considers software behavior in a rigorous and general way, e.g., to prove that (classes of) programs enjoy properties we want, and/or eschew properties we don’t. This approach has proven to be very valuable for solving a wide ranging set of problems. www.pl-enthusiast.net/2015/05/27/what-is-pl-research-and-how-is-it-useful/

Formal Semantics To assign mathematical meanings to language contructs programs A scientific way to study PL and programming -“developing general abstractions'” Formal Semantics of Prog.Lang. 09/07/2018

Formal Semantics • To assign mathematical meanings to language contructs & programs • A scientific way to study PL and programming – “developing general abstractions” Formal Semantics of Prog. Lang. 09/07/2018

Abstraction 南京地铁一号线 南京地二号线 南索地铁一号线南延线 十神电宝过 克间于四一计国H许-美 Formal Semantics of Prog.Lang. 09/07/2018

Abstraction Formal Semantics of Prog. Lang. 09/07/2018

Formal Semantics To assign mathematical meanings to language contructs programs A scientific way to study PL and programming -"developing general abstractions" -"considers software behavior in a rigorous and general way" ·More than testing Formal Semantics of Prog.Lang. 09/07/2018

Formal Semantics • To assign mathematical meanings to language contructs & programs • A scientific way to study PL and programming – “developing general abstractions” – “considers software behavior in a rigorous and general way” • More than testing Formal Semantics of Prog. Lang. 09/07/2018

factorial(n c=n; result 1; while (c>1){ result result c; C=c-1; return result; } Is it correct? What do we mean by correctness? Formal Semantics of Prog.Lang 09/07/2018

Formal Semantics of Prog. Lang. 09/07/2018 factorial( n ) { c = n; result = 1; while (c>1) { result = result * c; c = c-1; } return result; } Is it correct? What do we mean by correctness?

factorial(n This isn't right.It's not even wrong. (Wolfgang Pauli) izquotes.com What do we mean by correctness? Formal Semantics of Prog.Lang 09/07/2018

Formal Semantics of Prog. Lang. 09/07/2018 factorial( n ) { c = n; result = 1; while (c>1) { result = result * c; c = c-1; } return result; } Is it correct? What do we mean by correctness?

{n20} factorial(n { c =n; result 1; result n!/c!} while (c>1) resultresult c; C=c-1; } {result=n/c！c=1} return result; } result n! Formal Semantics of Prog.Lang. 09/07/2018

factorial( n ) { c = n; result = 1; while (c>1) { result = result * c; c = c-1; } return result; } Formal Semantics of Prog. Lang. 09/07/2018 { result = n!/c!} { result = n!/c!  c=1} { n  0 } { result = n! }