Fixed grammar.

This commit is contained in:
Amy J. Ko 2020-11-03 15:04:10 -08:00
parent c3b5ad3ad8
commit 5398afc9f6

View file

@ -62,4 +62,4 @@ The annotations above require that, no matter what, the inputs have to be intege
There are definite tradeoffs with writing detailed, formal specifications. The benefits are clear: many companies have written formal functional specifications in order to make _completely_ unambiguous the required behavior of their code, particularly systems that are capable of killing people or losing money, such as flight automation software, banking systems, and even compilers that create executables from code<woodcock09>. In these settings, it's worth the effort of being 100% certain that the program is correct because if it's not, people can die. Specifications can have other benefits. The very act of writing down what you expect a function to do in the form of test cases can slow developers down, causing to reflect more carefully and systematically about exactly what they expect a function to do<fucci16>. Perhaps if this is true in general, there's value in simply stepping back before you write a function, mapping out pre-conditions and post-conditions in the form of simple natural language comments, and _then_ writing the function to match your intentions. There are definite tradeoffs with writing detailed, formal specifications. The benefits are clear: many companies have written formal functional specifications in order to make _completely_ unambiguous the required behavior of their code, particularly systems that are capable of killing people or losing money, such as flight automation software, banking systems, and even compilers that create executables from code<woodcock09>. In these settings, it's worth the effort of being 100% certain that the program is correct because if it's not, people can die. Specifications can have other benefits. The very act of writing down what you expect a function to do in the form of test cases can slow developers down, causing to reflect more carefully and systematically about exactly what they expect a function to do<fucci16>. Perhaps if this is true in general, there's value in simply stepping back before you write a function, mapping out pre-conditions and post-conditions in the form of simple natural language comments, and _then_ writing the function to match your intentions.
Writing formal specifications can also have downsides. When the consequences of software failure aren't so high, the difficulty and time required to write and maintain functional specifications may not be worth the effort<petre13>. These barriers deter many developers from writing them<schiller14>. Formal specifications can also warp the types of data that developers work with. For example, it is much easier to write formal specifications about Boolean values and integers than string values. This can lead engineers to be overly reductive in how they model data (e.g., settling for binary models of gender, then gender is inherently non-binary and multidimensional). Writing formal specifications can also have downsides. When the consequences of software failure aren't so high, the difficulty and time required to write and maintain functional specifications may not be worth the effort<petre13>. These barriers deter many developers from writing them<schiller14>. Formal specifications can also warp the types of data that developers work with. For example, it is much easier to write formal specifications about Boolean values and integers than string values. This can lead engineers to be overly reductive in how they model data (e.g., using binary models of gender instead of more inclusive non-binary and multidimensional ones).