IU:TestPage
Revision as of 13:50, 9 February 2023 by R.sirgalina (talk | contribs)
-Calculus, Algebra, Machinery and Logic for Formal Program Semantics
- Course name: -Calculus, Algebra, Machinery and Logic for Formal Program Semantics
- Code discipline: CSE835
- Subject area: Software Engineering
Short Description
This elective course is designed for students in Computer Science, Software Engineering (IT more generally) and in Mathematics to catch main concepts formal program semantics and basic ideas from formal program specification and verification. We start with a make easy approach to formal semantics based on a toy language with esoteric operational, denotational, and logical (axiomatic) semantics. Then we move to operational, denotational, and axiomatic semantics for a simple imperative programming language.
Prerequisites
Prerequisite subjects
- CSE101, CSE102, CSE103, CSE104, CSE109
- CSE110 or CSE111 or CSE113 or CSE116
- CSE117, CSE119
Prerequisite topics
- natural, integer, rational, and real numbers
- functions and relations on numbers
- axiomatic method in geometry
- imperative (procedural) programming and languages
- algorithm complexity theory and data structures
- regular and context-free grammars and languages
- finite state machines (automata)
- basic programming skills
- basics of OOP software design
- familiarity with some development framework or technology (web or mobile)
Course Topics
| Section | Topics within the section |
|---|---|
| Section I: Course intro and Recall |
|
| Section II: Introduction to Program Semantics |
|
| Section III: Formal semantics for a simple imperative programming language |
|
| Section IV: λ-Calculus and Classical Denotational Semantics |
|
| Section V: Typed λ-Calculus and semantics of a simple functional language |
|
Intended Learning Outcomes (ILOs)
What is the main purpose of this course?
What is the main goal of this course formulated in one sentence? The main purpose of the course is to introduce the modern theory of programming languages.
ILOs defined at three levels
Level 1: What concepts should a student know/remember/explain?
By the end of the course, the students should be able to ...
- why we need formal semantics for programming languages
- principles of operational, denotational, and axiomatic approaches to formal semantics
- how to use of formal semantics for static analysis and formal verification
Level 2: What basic practical skills should a student be able to perform?
By the end of the course, the students should be able to ...
- define a operational, donotational, and axiomatic semantics for a simple imperative and functional programming language
- to specify formally and verify manually simple computational programs on a simple imperative or functional language.
Level 3: What complex comprehensive skills should a student be able to apply in real-life scenarios?
By the end of the course, the students should be able to ...
- problems with developing formal semantics for industrial programming languages.
- use of formal semantics for static analysis and formal verification.
- ways of introduction of formal semantics into Software engineering practice.
Grading
Course grading range
| Grade | Range | Description of performance |
|---|---|---|
| A. Excellent | 85.0-100.0 | - |
| B. Good | 75.0-84.0 | - |
| C. Satisfactory | 65.0-74.0 | - |
| D. Fail | 0.0-64.0 | - |
Course activities and grading breakdown
| Activity Type | Percentage of the overall course grade |
|---|---|
| Home-made problem-solving assignments for each of 5 sections of the course (10points for each assignment) | 50 |
| Individual in-class participation based on work in class (1 point for each class) | 10 |
| Final home-made written asynchronous examination | 40 |
Recommendations for students on how to succeed in the course
In-class participation is important (it implies attendance importance).
Topic-based regular home-made assignment are major grading item.
Please be aware that the lecture materials cover a plenty of topics from many sources, not a single one.
Resources, literature and reference materials
Open access resources
- Dijkstra E.W. A Discipline of Programming. Prentice-Hal, 1976.
- Gries D. The Science of Programming. Springer, 1987.
- Aaby A. Introduction to Programming Language. Working draft, 2004. Available at .
- Barendregt H. Lambda Calculi with Types. In: Handbook of Logic in Computer Science. Oxford University Press, 1992. Vol. II, pp. 117-309. Available at ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps.
- Shilov N.V. Introduction to Program Syntax, Semantics and Verification. (In Russian.) Novosibirsk State University, 2011. Draft is available at .
Closed access resources
- Not needed.
Software and tools used within the course
- Any compiler and IDE to implement, test, and exercise simple computational, search and sorting imperative and functional algorithms/programs.
Teaching Methodology: Methods, techniques, & activities
Activities and Teaching Methods
| Teaching Techniques | Section 1 | Section 2 | Section 3 | Section 4 | Section 5 |
|---|---|---|---|---|---|
| Problem-based learning (students learn by solving open-ended problems without a strictly defined solution) | 1 | 1 | 1 | 1 | 1 |
| Differentiated learning (provide tasks and activities at several levels of difficulty to fit students needs and level) | 1 | 1 | 1 | 1 | 1 |
| Contextual learning (activities and tasks are connected to the real world to make it easier for students to relate to them); | 1 | 1 | 1 | 1 | 1 |
| Развивающее обучение (задания и материал "прокачивают" ещё нераскрытые возможности студентов); | 1 | 1 | 1 | 1 | 1 |
| Концентрированное обучение (занятия по одной большой теме логически объединяются); | 1 | 1 | 1 | 1 | 1 |
| Learning Activities | Section 1 | Section 2 | Section 3 | Section 4 | Section 5 |
|---|---|---|---|---|---|
| Lectures | 1 | 1 | 1 | 1 | 1 |
| Interactive Lectures | 1 | 1 | 1 | 1 | 1 |
| Lab exercises | 1 | 1 | 1 | 1 | 1 |
| Flipped classroom | 1 | 1 | 1 | 1 | 1 |
| Quizzes (written or computer based) | 1 | 1 | 1 | 1 | 1 |
| Discussions | 1 | 1 | 1 | 1 | 1 |
Formative Assessment and Course Activities
Ongoing performance assessment
Section 1
| Activity Type | Content | Is Graded? |
|---|---|---|
| Home-made problem-solving assignment | Assume that , , and are sets. Prove without use of the power-set axiom that is a set. Prove without use of the set-union axiom that is a set. Prove (using extensionality postulate) uniqueness of the empty set uniqueness of the set for any given finite collection of sets of , … . Proof (using the enumeration and union postulate) existence of the standard union for all sets and . Proof (using the specification postulate) existence of the standard intersection for all sets and . Prove that for any set and any its subset the complement is a set. Proof (by contradiction using specification axiom) that collection usually called as the set of all sets isn’t a set. (Russel’s paradox.) |
1 |
Section 2
| Activity Type | Content | Is Graded? |
|---|---|---|
| Home-made problem-solving assignment | Is TEL a regular language? A context-free language? A context-sensitive language? A Recursively enumerable language? What will happen with TEL syntax (in terms of Chomsky classification) if it adopts spacing and indentation like Python? Assuming that all variables are of integer type and a conventional semantics for program answer what does this program compute? Validate that is indeed the operational semantics of TEL sentence . Prove that in TEL the following sentences and are equivalent. Prove that and are not equivalent in TEL. |
1 |
Section 3
| Activity Type | Content | Is Graded? |
|---|---|---|
| Home-made problem-solving assignment | Is ToyPL-VM language a context-free? Does it have a context-free syntax? Assuming a conventional program semantics and that the only data type is mathematical integers, try to guess (and prove somehow) what does compute the following ToyPL-VM program: 0: if z<0 then 1 else 2; 1: z:= -1 goto 8; 2: x:= 0 goto 3; 3: y:= 0 goto 4; 4: if y≤z then 5 else 7; 5: y:= y+2*x+1 goto 6; 6: x:= x+1 goto 4; 7: x:= x-1 goto 8; Let be any ToyPL-VM program, be any state of . Define by induction on structure of the expression (that uses variables in only) the value of this expression in this state . Let be any ToyPL-VM program, be any state of . Prove by induction on structure of the expression that for any expression (based on variables in ) the value of this expression in this state has a definite value. Validate that the implementation (semantics) of the ToyPL program from the left column is the ToyPL-VM program in right column. Select (always) valid assertions and explain your choice: |
1 |
Section 4
| Activity Type | Content | Is Graded? |
|---|---|---|
| Home-made problem-solving assignment | Is the language of the -Calculus regular? Context-free? The following sugared -term is representation of the following -term: List all free and bound variable instances in the -terms (a)-(e) from the previous exercise. Which of these -terms are combinators? Assuming the sugaring has no precedence, whether the desugaring of the -terms is confluent (i.e., always end with the same term)? Assuming the sugaring has the specified precedence, whether the desugaring of the -terms is confluent (i.e., always end with the same term)? Explain the following “proof” in the axiomatic semantics of the -Calculus and find a breach of the semantics: |
1 |
Section 5
| Activity Type | Content | Is Graded? |
|---|---|---|
| Home-made problem-solving assignment | Suggest any fix-point combinator other than . Write a Java-, Python-, etc. program that (being aware about its location) prints out its own code. Write yourself a quine-program in Java, Python, etc. Give example of a -term such that has a reduction graph that is a singleton with a single edge is a finite chain of length is an infinite chain Prove Church-Rosser theorem: If there are two distinct (-)reductions starting from a -term, then there exists a -term that is reachable from both reducts via a (possibly empty) sequence of (-)reductions. What is true: If a -term has a normal form, then its reduction graph is finite. If a -term has a finite reduction graph, then it has a normal form. Proof by induction of the height of the inference tree soundness of the axiomatic semantic of -Calculus: For any -terms and , if then there exists -term such that and . |
1 |
Final assessment
Section 1
- Can be a final exam, project defense, or some other equivalent of the final exam.
- The final examination is distance asynchronous individual written test to check that students understand and can apply main definitions, concepts and techniques presented on the lectures and available in lecture notes. The main grading criterions for written test will be human readable but concise, self-completeness, well-structuredness, and “proof of individual work” while computational (mainly arithmetic) errors will be treated as tiny mistakes (at most one-point deduction for each individual task).
- Examination has one (parameterized) variant for all enrolled students with 5 tasks with cost 8 points each (i.e., 40 points in total). “Human readable but concise” rule means that solutions should be well-commented but not exciding 1.5 (one and a half) pages each. Self-completeness means that the paper should be readable independently on any other resource, but lecture notes. Well-structuredness means that each task formulation, solution (proof if needed), answer (or conclusion) and its parts must be explicit in the paper and identified by appropriate headings/keywords (with respect to logical structure).
- Sample tasks follow.
- Task 1. Using definition of the natural number as in the lecture notes for section 1, construct the powerset for a given (specified) natural number . How many elements does it (the powerset) contains? (Explain all your answers.)
- Task 2. Using definitions from the lecture notes for section 2, construct a TEL “meaningful program” that after evaluation according to TEL informal semantics gets value , construct (step by step) its operational, denotational, and axiomatic semantics according to the TEL definitions. Here “meaningful” means that you can explain what does the program computes assuming a conventional informal program semantics. Please explain informally what this semantics is.
- Task 3. Using definitions from the lecture notes for section 3, and the same program as you construct in the exercise 2 above, construct (step by step) its operational and denotational semantics as a ToyPL program.
- Task 4. Using definitions from the lecture notes for section 3, and the same program as you construct in the exercise 2 above, specify the program by pre- and post-conditions according to your explanations (in the exercise 2) of what does the program compute, and then verify (using Floyd method or Hoare axiomatic semantics) correctness of the specified program.
- Task 5. Using definitions from the lecture notes for sections 4 & 5, construct a given (specified) natural number . Whether it is a combinator? Build reduction graph for . (Explain all your answers.)
Section 2
Section 3
Section 4
Section 5
The retake exam
Section 1
- Retake and re-examinations are designed to check that students understand and can apply main definitions, concepts and techniques covered in the lectures of the Course to overwrite grades for the final examination.
- Hybrid re-examination mode means that the examinations comprise a distance asynchronous individual written test (the first re-examination to be graded by Prof. N.V. Shilov) and an oral defense in front of a commission (consisting of Prof. N.V. Shilov and two more faculty to be appointed by the time of the second re-examination); format of the oral defense – offline or online – to be decided/arranged later (but prior to the defense date to be set by the Department of Education).
- Since (according to the Syllabus available the final examination costs 40 points, the cost of the re-examination is also 40 points. So, individual overall grade for the course after the retake for each participating student will be calculated according to the following formula , where is student’ overall score earned for the course during the teaching term, is student’ overall score earned for the final examination, is student’ score earned for the re-examination.
- Examination set comprises 5 individual tasks (but the same for both retakes) with cost points each (i.e., 40 points in total). “Human readable but concise” rule means that solutions should be well-commented but not exciding 1.5 (one and a half) pages each. Self-completeness means that the paper should be readable independently on any other resource, but lecture notes. Well-structuredness means that each task formulation, solution (proof if needed), answer (or conclusion) and its parts must be explicit in the paper and identified by appropriate headings/keywords (with respect to logical structure).
- Sample tasks follow.
- Task 1. Let us assume that ‘’, ‘‘, ‘’, and ‘’ are symbols. Using definition of the natural number as in the lecture notes on the topic 1, count (ignoring blank spaces) the length of the string thar represents a given natural number . How many elements does this representation contains? (Explain all your answers.)
- Task 2. Using definitions from the lecture notes on the topic 2, construct a TEL-program that in conventional (natural for a programming language) semantics computes (outputs) the integer part of the square root of a (input) positive integer, but that after evaluation according to TEL informal semantics gets value for a given natural number , construct (step by step) its operational, denotational, and axiomatic semantics according to the TEL definitions.
- Task 3. Using definitions from the lecture notes on the topic 3, and the same program as you construct in the exercise 2 above, construct (step by step) its implementation and denotational semantics as a ToyPL program.
- Task 4. Using definitions from the lecture notes on the topic 3, and the same program as you construct in the exercise 2 above, specify the program by pre- and post-conditions according to your explanations (in the exercise 2) of what does the program compute, and then verify (using Floyd method or Hoare axiomatic semantics) correctness of the specified program.
- Task 5. Using definitions from the lecture notes on the topics 4 and 5, construct explicitly the numeral for a given natural number . What is type of the numeral Demonstrate that . What is type of the term ? Build reduction graph for . (Explain all your answers.)
Section 2
Section 3
Section 4
Section 5