形式化方法是一种基于数学的软件和系统开发方法，研究如何把（具有清晰的数学基础的）严格性（描述形式、技术和过程等）融入软件开发的各个阶段：规范、设计、验证与演化等。该方法日益受到计算机界和工业界的高调重视。形式化方法是计算机专业一门重要的专业基础课，特别是计算机科学专业必修课，也是软件工程专业和信息管理专业一门重要的基础课。通过本课程的学习，使学生了解形式化方法的基本理论和基本原理，掌握软件形式规格，能应用基本形式化方法验证程序正确性。学会用“数学思维”去思考和用“形式化方法”去处理软件和系统开发过程的程序验证问题。