FI:I022 Programming and Logic - Course Information

I022 Programming and Logic

Extent and Intensity

2/0. 2 credit(s). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium), z (credit).

Teacher(s)

prof. RNDr. Luboš Brim, CSc. (lecturer)

Guaranteed by

Contact Person: prof. RNDr. Luboš Brim, CSc.

Course Enrolment Limitations

The course is also offered to the students of the fields other than those the course is directly associated with.

fields of study / plans the course is directly associated with

• Informatics (programme FI, B-IN)
• Informatics (programme FI, M-IN)
• Upper Secondary School Teacher Training in Informatics (programme FI, M-IN)
• Upper Secondary School Teacher Training in Informatics (programme FI, M-SS)
• Information Technology (programme FI, B-IN)

Syllabus

• Propositions and predicates, reasoning within first-order logic, bounded quantification, textual substitution.
• Programs as predicate transformers, weakest precondition, properties of predicate transformers.
• Garded command language. Skip and abort commands, composition, alternative command, iterative command.
• Verification of programs, proof outlines, verification rules.
• Constructive verification of programs, basic principles and strategies, developing loops from invariants and bounds, developing invarinats.
• Examples of program development.

Language of instruction

Czech

• Enrolment Statistics (Autumn 1997, recent)
  
• Permalink: https://is.muni.cz/course/fi/autumn1997/I022