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. Read syllabus. 20minutes
2． Hoare logic 1
Assertions and programs 		Reviewing contents of the class. 30minutes
3． Hoare logic 2
Partial correctness and total correctness 		Reviewing contents of the class. 30minutes
4． Hoare locic 3
proving correctness of simple programs. 		Reviewing contents of the class. 30minutes
5． Hoare logic 4
Proving correctness of programs with iteration 1.. 		Reviewing contents of the class. 30minutes
6． Hoare logic 5
Proving correctness of programs with iteration 2 		前回までの内容をよく理解しておくこと 30minutes
7． Hoare logic 6
Proving correctness of programs with conditionals. 		Reviewing contents of the class. 30minutes
8． Hoare logic 7
Proving correctness of complicated programs. 		Reviewing contents of the class. 30minutes
9． Hoare logic 8
Total correctness and its proof. 		Reviewing contents of the class. 30minutes
10． Hoare logic 9
Limitation of Hoare logic 		Reviewing contents of the class. 30minutes
11． Dijkstra method 1
Weakest pre-conditoin and adding assertions to programs. 		Reviewing contents of the class. 30minutes
12． Dijkstra method 2
Proving correctness of non-deterministic programs. 		Reviewing contents of the class. 30minutes
13． Verification of various programs 1
programs with arrays 		Reviewing contents of the class. 30minutes
14． Verification of various programs 2
programs with local variables
Verification and types. 		Reviewing contents of the class. 30minutes
Total. - - 410minutes
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
Relation to the environment
Non-environment-related course
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 applicatable
N/A N/A
Last modified : Thu Mar 21 14:59:47 JST 2019