1 false COMP2600 <p>This course presents some formal notations that are commonly used for the description of computation and of computing systems, for the specification of software and for mathematically rigorous arguments about program properties.<br />The following areas of study constitute the backbone of the course. Predicate calculus and natural deduction, inductive definitions of data types as a basis for recursive functions and structural induction, formal language theory (particularly regular expressions, finite state machines and context free grammars), specification languages, propositional programming language semantics, partial correctness and proofs of termination.</p> B 1 false 10775 <p>Assignments (40%); Tutorials and Laboratories (5%); Quiz (10%); Final Exam (45%)</p> 1 1 <p>Upon completion of this course, the student will be able to do the following. </p><ol><li>Apply the concepts of standard mathematical logic to produce proofs or refutations of well-formed propositions or arguments phrased in English or in a variety of formal notations (first order logic, discrete mathematics or Hoare Logic). </li><li>Given a description of a regular language, either in English, as a regular expression or as a grammar, generate a finite state automaton that recognizes that language. Similarly, given a deterministic or nondeterministic automaton, give a description of the language which it accepts. </li><li>Given an inductive definition of a simple data structure, write a recursive definition of a given simple operation on data of that type. Given some such recursively defined operations, prove simple properties of these functions using the appropriate structural induction principle.</li><li>Prove simple programs correct using Hoare Logic. </li><li>Prove correctness and termination of a simple program using the weakest precondition calculus. </li><li>Specify a simple system using Z. </li><li>Understand very simple Prolog programs.</li><li>Design a Turing Machine which will accomplish simple tasks. </li></ol> 0 Formal Methods in Software Engineering 6 6 <p>There is no prescribed text for COMP2600, but the following are recommended references. More may be added as the semester progresses.</p><p> Grassman, Winfried Karl Grassman &amp; Tremblay, Jean-Paul <em>Logic and Discrete Mathematics: A Computer Science Perspective</em>, Prentice Hall, Upper Saddle River, New Jersey, 1996.</p><p> Thompson, Simon <em>Haskell: The Craft of Functional Programming</em>, International Computer Science Series. Addison-Wesley, Wokingham, England, 1999.</p><p> Epp, Susanna S. <em>Discrete Mathematics with Applications</em>Computer Science Press, New York, 1995.</p><p> Bergmann, Merrie <em>The Logic Book</em>, McGraw-Hill.</p><p> Munro, John <em>Discrete Mathematics for Computing </em>Thomas Nelson.</p> 6 <p>COMP1110 or COMP1510 or COMP2750 and&nbsp; MATH1005 or MATH1014 or MATH1116 or enrolment in&nbsp; Bachelor of Computer Science Honours</p> Form Meth Software Engn Band 2 Computer Science <p>Thirty one-hour lectures, eight one-hour tutorials and four two-hour laboratory sessions.</p> 2010