Fixed typo.

This commit is contained in:
Amy J. Ko 2020-11-03 15:01:10 -08:00
parent 42151f87f5
commit c3b5ad3ad8

View file

@ -48,7 +48,7 @@ These two new lines of code are essentially functional specifications that decla
Assertions are related to the broader category of *error handling* language features. Error handling includes assertions, but also programming language features like exceptions and exception handlers. Error handling is a form of specification in that _checking_ for errors usually entails explicitly specifying the conditions that determine an error. For example, in the code above, the condition `Number.isInteger(a)` specifies that the parameter `a` must be an integer. Other exception handling code such as the Java `throws` statement indicates the cases in which errors can occur and the corresponding `catch` statement indicates what is to done about errors. It is difficult to implement good exception handling that provides granular, clear ways of recovering from errors<chen09>. Evidence shows that modern developers are still exceptionally bad at designing for errors; one study found that errors are not designed for, few errors are tested for, and exception handling is often overly general, providing little ability for users to understand errors or for developers to debug them<ebert15>. These difficulties appear to be because it is difficult to imagine the vast range of errors that can occur<maxion00>.
Researchers have invented many forms of specification that require more work and more thought to write, but can be used to make stronger guarantees about correctness<woodcock09>. For example, many languages support the expression of formal *pre-conditions* and *post-conditions* that represent contracts that must be kept for the program to be corect. (*Formal* means mathematical, facilitating mathematical proofs that these conditions are met). Because these contracts are essentially mathematical promises, we can build tools that automatically read a function's code and verify that what it computes exhibits those mathematical properties using automated theorem proving systems. For example, suppose we wrote some formal specifications for our example above to replace our assertions (using a fictional notation for illustration purposes):
Researchers have invented many forms of specification that require more work and more thought to write, but can be used to make stronger guarantees about correctness<woodcock09>. For example, many languages support the expression of formal *pre-conditions* and *post-conditions* that represent contracts that must be kept for the program to be correct. (*Formal* means mathematical, facilitating mathematical proofs that these conditions are met). Because these contracts are essentially mathematical promises, we can build tools that automatically read a function's code and verify that what it computes exhibits those mathematical properties using automated theorem proving systems. For example, suppose we wrote some formal specifications for our example above to replace our assertions (using a fictional notation for illustration purposes):
`javascript
// pre-conditions: a in Integers, b in Integers