I022 Programming and Logic

Faculty of Informatics
Autumn 1996
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
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
The course is also listed under the following terms Autumn 1995, Autumn 1997, Autumn 1998, Autumn 1999, Autumn 2000, Autumn 2001.
  • Enrolment Statistics (Autumn 1996, recent)
  • Permalink: https://is.muni.cz/course/fi/autumn1996/I022