Course title
1M9780001
Programming Languages

 aiba akira Click to show questionnaire result at 2017
Course content
Programming languages are tools for using computers. Nowadays there are many kinds of programming languages and they are divided into several programming paradigms.
In this class students will learn "Program verification" to understand mathematical handling of programs. Program verification is ways of proving correctness of programs in mathematical ways.
Purpose of class
Understanding theoretical aspects of programming languages.
Goals and objectives
  1. Students are expected to learn theoretical handling of programs and programming languages.
  2. Students are expected to understand basic theory of programming languages.
  3. Students are expected to understand program verification.
Language
Japanese
Class schedule

 Class schedule HW assignments (Including preparation and review of the class.) Amount of Time Required
1． What is program verification. Think about why mathematical consideration of programs is needed 40minutes
Summarize how you have confirmed the correctness of the program you programmed 60minutes
Review the basics of Symbolic Logic 180minutes
2． Hoare logic 1
Assertions and programs 		Reviewing contents of the previous class. 100minutes
3． Hoare logic 2
Partial correctness and total correctness 		Reviewing contents of the previous class. 180minutes
4． Hoare locic 3
proving correctness of simple programs. 		Reviewing contents of the previous class. 180minutes
5． Hoare logic 4
Proving correctness of programs with iteration 1.. 		Reviewing contents of the previous class. 180minutes
6． Hoare logic 5
Proving correctness of programs with iteration 2 		Reviewing contents of the previous class. 180minutes
7． Hoare logic 6
Proving correctness of programs with conditionals. 		Reviewing contents of the previous class. 180minutes
8． Hoare logic 7
Proving correctness of complicated programs. 		Reviewing contents of the previous class. 200minutes
9． Hoare logic 8
Total correctness and its proof. 		Reviewing contents of the previous class. 200minutes
10． Hoare logic 9
Limitation of Hoare logic 		Reviewing contents of the previous class. 200minutes
11． Dijkstra method 1
Weakest pre-conditoin and adding assertions to programs. 		Reviewing contents of the previous class. 200minutes
12． Dijkstra method 2
Proving correctness of non-deterministic programs. 		Reviewing contents of the previous class. 200minutes
13． Verification of various programs 1
programs with arrays 		Reviewing contents of the previous class. 200minutes
14． Verification of various programs 2
programs with local variables
Verification and types. 		Reviewing contents of the previous class. 200minutes
Total. - - 2680minutes
Relationship between 'Goals and Objectives' and 'Course Outcomes'

 Report Total.
1. 30% 30%
2. 30% 30%
3. 40% 40%
Total. 100% -
Evaluation method and criteria
Students are evaluated by reports.
Textbooks and reference materials
Reference
S. Hayashi, "Program verification (in Japanese)", kyouritu-shuppan , 1998.
Prerequisites
Not specified.
Office hours and How to contact professors for questions
  • Tuesday, 12:30 - 13:00
Regionally-oriented
Non-regionally-oriented course
Development of social and professional independence
  • Non-social and professional independence development course
Active-learning course
N/A
Course by professor with work experience
Work experience Work experience and relevance to the course content if applicable
N/A N/A
Education related SDGs:the Sustainable Development Goals
  • 4.QUALITY EDUCATION
  • 9.INDUSTRY, INNOVATION AND INFRASTRUCTURE
Last modified : Wed Mar 24 04:10:43 JST 2021