Editing Formal methods (section)

==Uses==

Formal methods can be applied at various points through the [[software development process|development process]].

===Specification===
{{Main|Formal specification}}
Formal methods may be used to give a formal description of the system to be developed, at whatever level of detail desired. Further formal methods may depend on this specification to synthesize a program or to verify the correctness of a system. 

Alternatively, specification may be the only stage in which formal methods is used. By writing a specification, ambiguities in the informal requirements can be discovered and resolved. Additionally, engineers can use a formal specification as a reference to guide their development processes.<ref>{{cite journal|last1=Utting|first1=Mark|last2=Reeves|first2=Steve|date=August 31, 2001|title=Teaching formal methods lite via testing|url=https://onlinelibrary.wiley.com/doi/abs/10.1002/stvr.223|journal=Software Testing, Verification and Reliability|volume=11|issue=3|pages=181–195 |doi=10.1002/stvr.223}}</ref>

The need for formal specification systems has been noted for years. In the [[ALGOL 58]] report,<ref>{{cite conference | first = J.W. | last = Backus | title = The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference | book-title = Proceedings of the International Conference on Information Processing | publisher = UNESCO | year = 1959 }}</ref> [[John Backus]] presented a formal notation for describing [[Syntax (programming languages)|programming language syntax]], later named [[Backus normal form]] then renamed [[Backus–Naur form]] (BNF).<ref>[[Donald Knuth|Knuth, Donald E.]] (1964), Backus Normal Form vs Backus Naur Form. ''[[Communications of the ACM]]'', 7(12):735–736.</ref> Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs was not completed in time for inclusion in the report, stating that it "will be included in a subsequent paper." However, no paper describing the formal semantics was ever released.<ref>{{cite book|last1=O'Hearn|first1=Peter W.|last2=Tennent|first2=Robert D.|title=Algol-like Languages|date=1997}}</ref>

===Synthesis===
{{Main|Program synthesis}}
Program synthesis is the process of automatically creating a program that conforms to a specification. Deductive synthesis approaches rely on a complete formal specification of the program, whereas inductive approaches infer the specification from examples. Synthesizers perform a search over the space of possible programs to find a program consistent with the specification. Because of the size of this search space, developing efficient search algorithms is one of the major challenges in program synthesis.<ref>{{cite journal|last1=Gulwani|first1=Sumit|last2=Polozov|first2=Oleksandr|last3=Singh|first3=Rishabh|date=2017|title=Program Synthesis|url=https://www.nowpublishers.com/article/Details/PGL-010|journal=Foundations and Trends in Programming Languages|volume=4|issue=1–2|pages=1–119 |doi=10.1561/2500000010 }}</ref>

===Verification===
{{Main|Formal verification}}
Formal verification is the use of software tools to prove properties of a formal specification, or to prove that a formal model of a system [[implementation]] satisfies its specification.

Once a formal specification has been developed, the specification may be used as the basis for [[mathematical proof|proving]] properties of the specification, and by inference, properties of the system implementation.

==== Sign-off verification ====
Sign-off verification is the use of a formal verification tool that is highly trusted.  Such a tool can replace traditional verification methods (the tool may even be certified).{{citation needed|date=June 2024}}

====Human-directed proof====
Sometimes, the motivation for proving the [[correctness (computer science)|correctness]] of a system is not the obvious need for reassurance of the correctness of the system, but a desire to understand the system better. Consequently, some proofs of correctness are produced in the style of [[mathematical proof]]: handwritten (or typeset) using [[natural language]], using a level of informality common to such proofs. A "good" proof is one that is readable and understandable by other human readers.

Critics of such approaches point out that the [[ambiguity]] inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the low-level details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.

====Automated proof====
In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into three general categories:
* [[Automated theorem proving]], in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical [[axiom]]s, and a set of [[Rule of inference|inference rules]].
* [[Model checking]], in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution.
* [[Abstract interpretation]], in which a system verifies an over-approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete) [[lattice (order theory)|lattice]] representing it.

Some [[Automated theorem proving|automated theorem provers]] require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model.

Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners.

Critics note that some of those systems are like [[Oracle machine|oracle]]s: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "[[Quis custodiet ipsos custodes?|verifying the verifier]]"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification.

The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators<ref>A. Cortesi and M. Zanioli, [http://www.dsi.unive.it/~cortesi/paperi/CL_2011.pdf Widening and Narrowing Operators for Abstract Interpretation]. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, {{ISSN|1477-8424}} (2011).</ref> to get fast convergence.