This course aims to introduce formal software specification. The main contents include formal specification language, requirements specification, pre and post conditions, formal software design modeling, formal verification and model checking tools with some practical case studies.