Added language annotations.

chapters/specifications.md

@@ -6,7 +6,7 @@ The techniques we've discussed so far for avoiding this boil down to _specifying
 
 In their simplest form, a functional specification can be a just some natural language that says what an individual function is supposed to do:
 		
-`
+`javascript
 // Return the smaller of the two numbers, 
 // or if they're equal, the second number.
 function min(a, b) {
@@ -20,7 +20,7 @@ The comment above is okay, but it's not very precise. It says what is returned a
 		
 To make these clearer, many languages use *static typing* to allow developers to specify types explicitly:
 
-`
+`javascript
 // Return the smaller of the two integers, or if they're equal, the second number.
 function min(int a, int b) {
   return a < b ? a : b;
@@ -33,7 +33,7 @@ Of course, if the above was JavaScript code (which doesn't support static typing
 		
 This brings us to a second purpose of writing functional specifications: to help _verify_ that functions, their input, and their output are correct. Tests of functions and other low-level procedures are called *unit tests*. 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 *assertions*<clarke06>. 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:
 		
-`
+``javascript
 // Return the smaller of the two numbers, or if they're equal, the second number.
 function min(a, b) {
   if(!Number.isInteger(a)) 
@@ -50,7 +50,7 @@ Assertions are related to the broader category of *error handling* language feat
 		
 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):
 
-`
+`javascript
 // pre-conditions: a in Integers, b in Integers
 // post-conditions: result <= a and result <= b
 function min(a, b) {

chapters/verification.md

@@ -25,7 +25,7 @@ Why is this? One possibility is that *no amount of testing can prove a program c
 		
 Consider this JavaScript program:
 
-`
+`javascript
 function count(input) {
   while(input > 0)
     input--;
@@ -57,7 +57,6 @@ The benefits of analysis is that it _can_ demonstrate that a program is correct
 		
 One popular type of automatic program analysis tools is a *static analysis* tool. These tools read programs and identify potential defects using the types of formal proofs like the ones above. They typically result in a set of warnings, each one requiring inspection by a developer to verify, since some of the warnings may be false positives (something the tool thought was a defect, but wasn't). Although static analysis tools can find many kinds of defects, they aren't yet viewed by developers to be that useful because the false positives are often large in number and the way they are presented make them difficult to understand<johnson13>. There is one exception to this, and it's a static analysis tool you've likely used: a compiler. Compilers verify the correctness of syntax, grammar, and for statically-typed languages, the correctness of types. As I'm sure you've discovered, compiler errors aren't always the easiest to comprehend, but they do find real defects automatically. The research community is just searching for more advanced ways to check more advanced specifications of program behavior.
 
-
 Not all analytical techniques rely entirely on logic. In fact, one of the most popular methods of verification in industry are *code reviews*, also known as _inspections_. The basic idea of an inspection is to read the program analytically, following the control and data flow inside the code to look for defects. This can be done alone, in groups, and even included as part of process of integrating changes, to verify them before they are committed to a branch. Modern code reviews, while informal, help find defects, stimulate knowledge transfer between developers, increase team awareness, and help identify alternative implementations that can improve quality<bacchelli13>.  One study found that measures of how much a developer knows about an architecture can increase 66% to 150% depending on the project<rigby13>. That said, not all reviews are created equal: the best ones are thorough and conducted by a reviewer with strong familiarity with the code<kononenko16>; including reviewers that do not know each other or do not know the code can result in longer reviews, especially when run as meetings<seaman97>. Soliciting reviews asynchronously by allowing developers to request reviewers of their peers is generally much more scalable<rigby11>, but this requires developers to be careful about which reviews they invest in. These choices about where to put reviewing attention can result in great disparities in what is reviewed, especially in open source: the more work a review is perceived to be, the less likely it is to be reviewed at all and the longer the delays in receiving a review<thongtanunam16>.		
 
 Beyond these more technical considerations around verifying a program's correctness are organizational issues around different software qualities. For example, different organizations have different sensitivities to defects. If a $0.99 game on the app store has a defect, that might not hurt its sales much, unless that defect prevents a player from completing the game. If Boeing's flight automation software has a defect, hundreds of people might die. The game developer might do a little manual play testing, release, and see if anyone reports a defect. Boeing will spend years proving mathematically with automatic program analysis that every line of code does what is intended, and repeating this verification every time a line of code changes. Moreover, requirements may change differently in different domains. For example, a game company might finally recognize the sexist stereotypes amplified in its game mechanics and have to change requirements, resulting in changed definitions of correctness, and the incorporation of new software qualities such as bias into testing plans. Similarly, Boeing might have to respond to pandemic fears by having to shift resources away from verifying flight crash safety to verifying public health safety. What type of verification is right for your team depends entirely on what a team is building, who's using it, and how they're depending on it.