May 26, 2026  
2025-2026 Undergraduate Catalog 
    
2025-2026 Undergraduate Catalog

CS 471 - Program Derivation



Introduction to the formal derivation of computer programs from program specifications. Review of the logical and notational prerequisites needed for formal derivation. Guarded commands and the predicate transformer WP. Developing loops from invariants. Program development via sequence of refinements.

Credits: 3
Prerequisites:   and  . Prerequisites must be completed with a grade of C or better.  The maximum number of attempts for this course is three, including earned grades, withdrawals, and audits.
Notes:  This course is crosslisted with CS 671. Credit at the 600-level requires additional work.