In this chapter, the following content will be discussed: Cleanroom process teams, free and bound variables, universal quantification, one point rule, data structures, binary relations, relational calculus, operator symbols. | Formal Methods in SE Qaisar Javaid Assistant Professor Specification team. Responsible for developing and maintaining the system specification. Development team. Responsible for developing and verifying the software. The software is NOT executed or even compiled during this process. Certification team. Responsible for developing a set of statistical tests to exercise the software after development. Reliability growth models used to determine when reliability is acceptable. Cleanroom process teams The results of using the Cleanroom process have been very impressive with few discovered faults in delivered systems. Independent assessment shows that the process is no more expensive than other approaches. There were fewer errors than in a 'traditional' development process. However, the process is not widely used. It is not clear how this approach can be transferred to an environment with less skilled or less motivated software engineers. Cleanroom process evaluation Free and Bound Variables In the expression Q x : A/B • p we say that variable x is bound by the quantifier. The scope of x extends from the vertical bar (or the spot if there is no constraint) to the next closing bracket. If the variable x appears in a predicate q but is not bound by any quantifier, we say that x is free in q. Substitution We write p[t/x ] to denote the predicate that results from substituting t for each free occurrence of x in predicate p. The substitute expression t need not be another variable; it can be any expression whose possible values match those of x. Universal Quantification The universal quantifier ∀ is a generalized form of ∧. Existential Quantification The existential quantifier ∃ is a generalized form of ∨. Universal Quantification Existential Quantification Equality The = (equality) symbol is used to show that expressions are identical Equalities are one form of atomic propositions in our logical language (the other form is set membership). | Formal Methods in SE Qaisar Javaid Assistant Professor Specification team. Responsible for developing and maintaining the system specification. Development team. Responsible for developing and verifying the software. The software is NOT executed or even compiled during this process. Certification team. Responsible for developing a set of statistical tests to exercise the software after development. Reliability growth models used to determine when reliability is acceptable. Cleanroom process teams The results of using the Cleanroom process have been very impressive with few discovered faults in delivered systems. Independent assessment shows that the process is no more expensive than other approaches. There were fewer errors than in a 'traditional' development process. However, the process is not widely used. It is not clear how this approach can be transferred to an environment with less skilled or less motivated software engineers. Cleanroom process evaluation Free and Bound
