Clarifications of unit tests and formallity.

specifications.html

@@ -33,7 +33,7 @@
 		
 		<p>The techniques we've discussed so far for avoiding this boil down to <em>specifying</em> what code should do, so everyone can write code according to a plan. We've talked about <a href="requirements.html">requirements specifications</a>, which are declarations of what software must do from a users' perspective. We've also talked about <a href="architecture.html">architectural specifications</a>, which are high-level declarations of how code will be organized, encapsulated, and coordinated. At the lowest level are <b>functional specifications</b>, which are declarations about the <em>properties of input and output of functions in a program</em>.
 
-		<p>In their simplest form, a functional specification can be just some natural language that says what a function is supposed to do:</p>
+		<p>In their simplest form, a functional specification can be a just some natural language that says what an individual function is supposed to do:</p>
 		
 		<pre>
 // Return the smaller of the two numbers, or if they're equal, the second number.
@@ -59,7 +59,7 @@ function min(int a, int b) {
 
 		<p>Of course, if the above was JavaScript code (which doesn't support static typing), JavaScript does nothing to actually verify that the data given to <code>min()</code> are actually integers. It's entirely fine with someone sending a string and an object. This probably won't do what you intended, leading to defects.</p>
 		
-		<p>This brings us to a second purpose of writing functional specifications: to help <em>verify</em> that functions, their input, and their output are correct. There are many ways to use specifications to verify correctness. By far, one of the most widely used is <b>assertions</b> (<a href="#clarke">Clarke & Rosenblum 2006</a>). Assertions consist of two things: 1) a check on some property of a function's input or output and 2) some action to notify about violations of these properties. For example, if we wanted to verify that the JavaScript function above had integer values as inputs, we would do this:</p>
+		<p>This brings us to a second purpose of writing functional specifications: to help <em>verify</em> that functions, their input, and their output are correct. Tests of functions and other low-level procedures are called <strong>unit tests</strong>. There are many ways to use specifications to verify correctness. By far, one of the simplest and most widely used kinds of unit tests are <b>assertions</b> (<a href="#clarke">Clarke & Rosenblum 2006</a>). Assertions consist of two things: 1) a check on some property of a function's input or output and 2) some action to notify about violations of these properties. For example, if we wanted to verify that the JavaScript function above had integer values as inputs, we would do this:</p>
 		
 		<pre>
 // Return the smaller of the two numbers, or if they're equal, the second number.
@@ -74,7 +74,7 @@ function min(a, b) {
 		
 		<p>Assertions are related to the broader category of <strong>error handling</strong> 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 <em>checking</em> for errors usually entails explicitly specifying the conditions that determine an error. For example, in the code above, the condition <code>Number.isInteger(a)</code> specifies that the parameter <code>a</code> must be an integer. Other exception handling code such as the Java <code>throws</code> statement indicates the cases in which errors can occur and the corresponding <code>catch</code> 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 (<a href="#chen">Chen et al. 2009</a>). 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 (<a href="#ebert">Ebert et al. 2015</a>). These difficulties appear to be because it is difficult to imagine the vast range of errors that can occur (<a href="#maxion">Maxion & Olszewski 2000</a>).</p>
 		
-		<p>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 (<a href="#woodcock">Woodcock et al. 2009</a>). For example, many languages support the expression of formal <strong>pre-conditions</strong> and <strong>post-conditions</strong> that represent contracts that must be kept. 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):</p>
+		<p>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 (<a href="#woodcock">Woodcock et al. 2009</a>). For example, many languages support the expression of formal <strong>pre-conditions</strong> and <strong>post-conditions</strong> that represent contracts that must be kept. (<strong>Formal</strong> 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):</p>
 		
 		<pre>
 // pre-conditions: a in Integers, b in Integers

verification.html

@@ -85,7 +85,7 @@ function count(input) {
 		<p>There are many types of testing that are common in software engineering:</p>
 		
 		<ul>
-			<li><strong>Unit tests</strong> verify that low-level functions return the correct output. For example, a program that implemented a function for finding the day of the week for a given date might also include unit tests that verify for a large number of dates that the correct day of the week is returned. They're good for ensuring widely used low-level functionality is correct.</li>
+			<li><strong>Unit tests</strong> verify that functions return the correct output. For example, a program that implemented a function for finding the day of the week for a given date might also include unit tests that verify for a large number of dates that the correct day of the week is returned. They're good for ensuring widely used low-level functionality is correct.</li>
 			<li><strong>Integration tests</strong> verify that when all of the functionality of a program is put together into the final product, it behaves according to specifications. Integration tests often operate at the level of user interfaces, clicking buttons, entering text, submitting forms, and verifying that the expected feedback always occurs. Integration tests are good for ensuring that important tasks that users will perform are correct.</li>
 			<li><strong>Regression tests</strong> verify that behavior that previously worked doesn't stop working. For example, imagine you find a defect that causes logins to fail; you might write a test that verifies that this cause of login failure does not occur, in case someone breaks the same functionality again, even for a different reason. Regression tests are good for ensuring that you don't break things when you make changes to your application.</li>
 		</ul>