Lecture
1 The concept of survivability of a system (any system) - Survivability
2 The concept of survivability in communication systems
3 The concept of liveness in parallel computing - Liveness
4 Persistence in OOP
5. Survivability in software - Robustness -( reliability)
6 Survivability (Persistence) in computer science - Persistence (computer science)
7 A theorem describing the set of behaviors by means of the safety property (safety) and the liveness property (liveness)
The notion of liveness in the broad sense is closely related to the notion of system survivability; in narrower senses (often simultaneously) it appears in narrower fields such as databases, OOP, parallel computing, networks, software, computer science, etc. Because different English-language terms share the same translation liveness - identification difficulties may arise; context helps to resolve them.
Let us examine comprehensively some notions of liveness in these narrower senses.
In [ 5 ], survivability is understood as “the property of a communication system to retain and restore its ability to perform its basic functions within a specified scope and for a specified operating time when the system's structure and (or) algorithms and operating conditions change owing to adverse effects”. Survivability characterizes the resilience of a communication network against causes lying outside the network that lead to the destruction or significant damage of some of its parts. Survivability – the property of a network to retain the ability to perform required functions under conditions created by the action of external destabilizing factors [ 6 ].
Survivability — the ability of a technical device, structure, facility, or system to perform its basic functions despite damage sustained, or by adapting to new conditions.
For example, the survivability of a ship can be understood as its ability to remain afloat and not lose stability in the event of flooding of one or more compartments due to hull damage.
The survivability of an urban electric transit system is defined by its ability not to interrupt the operation of the whole system, or of a significant section of it, because of scheduled repairs, an accident, or damage to the contact network and/or the track. When difficulties arise, routes are diverted onto bypass paths, shortened by using intermediate turning loops, or redirected to a reserve terminal station. For trolleybuses, the use of autonomous propulsion systems is also possible. In cases where a route cannot operate on a section for an extended period (repairs) — temporary electric transit routes and compensating bus routes are introduced. In some cases, when a branch section is connected to the main network by a single line (via a bridge, for example) — an effort is made to design a dedicated depot for that section. If there is none, temporary sites are set up for overnight storage of rolling stock. In the case of trams, when a section blocked for a long period has no turning loop, shuttle working is used — cars coupled tail to tail.
The survivability of a gun barrel (liner) is defined as the number of rounds the gun can fire before it fails or its shot grouping degrades to an unacceptable level.
In [ 4 ], the survivability of a communication system is understood as “the resistance of a communication system to damage of its elements by natural factors and deliberate enemy actions”. In [ 7 ], survivability is defined with respect to a military communication system as: “The ability of a military communication system to provide command and control of troops or forces and weapons under conditions of enemy weapons employment”
"The capability of a system to fulfill its mission, in a timely manner, in the presence of threats such as attacks or large-scale natural disasters. Survivability is a subset of resilience."[ 1 ][ 2 ]
“The capability of a system to fulfill its mission, in a timely manner, in the presence of attacks, failures, or accidents.”
Computer networks use the so-called Stop-and-Wait protocol. Proving its correctness consists of proving –
GUARANTEE (safety) : packets are delivered strictly in order and no packet duplication occurs (each packet is delivered exactly once) –
and LIVENESS (liveness) : eventually, all packets are delivered (no packets are lost).
Models for the quantitative assessment of network survivability and connectivity probability have been developed since the middle of the last century and have since seen extensive development. When determining the connectivity probability of a network, it is assumed that the network contains redundant arcs (compared with a tree) whose failure is permissible. Any damage to a tree-like network leads to a loss of connectivity, and survivability becomes equal to zero. But an analysis of attacks on networks shows that networks continue to function even if they have broken up into fragments. This has created a need to develop methods and models of network survivability that account for modern operating conditions.
Structural survivability, expressed through the mathematical expectation of the number of failed nodes, reflects the topology of the network.
Functional survivability, expressed through the mathematical expectation of the number of surviving connections (inter-node flows), is a reflection of the flow characteristics of the network: the distribution of path lengths, the total and average path length, the average arc load, and the total number of connections.
Flow-based survivability makes it possible to assess the load on arcs both before and after an attack on redundant arcs, and to establish the bandwidth reserve needed in case of the loss of redundant arcs.
The figure shows a classification (tree) of the properties that determine the survivability of ITS (INFORMATION AND TELECOMMUNICATION SYSTEMS) .
Fig. Classification (tree) of the properties determining the survivability of ITS
The properties listed above give rise to the corresponding individual survivability indicators of ITS.
Structural survivability — the property of a system to retain the performance of its functions at least at a minimally acceptable level for a required period of time under passive resistance to damage of the system's elements.
Functional survivability — the property of a system to retain the required level of operability owing to the adopted algorithm for controlling the routing
of information exchange between the system's subscribers, or its reconfiguration.
Technical survivability — the property of a system to retain the performance of its functions owing to the restoration of the operability of its elements.
Element survivability — the property of ITS elements characterizing their resistance to damaging factors and their ability to restore operability
Reconnaissance resistance in this case is also one of the individual survivability properties of ITS.
Let us note that the set of properties shown in the figure is not closed; it can be extended or narrowed. This is determined by the system of views
(principles) adopted for ensuring the survivability of ITS.
In a concurrent computation, liveness refers to a set of properties of concurrent systems that require a system to keep making progress, despite the fact that its simultaneously executing components ( «processes») may have to take turns «one after another» in critical sections, parts of the program that cannot be run by several processes at the same time. Liveness guarantees are important properties in operating systems and distributed systems .
In more general terms, a liveness property states that «something good will eventually happen», as opposed to a safety property, which states that «something bad never happens». If a safety property is violated, this is always shown by a finite execution that exhibits the violation (a «bad» event occurring), but a liveness property can never be shown to be violated by a finite execution of a distributed system, since the «good» event may still occur at some later time. Eventual consistency is an example of a liveness property. Any property can be expressed as the intersection of safety properties and liveness properties. Whereas a violation of a given safety property admits a finite witness, a violation of a liveness property can be harder to establish, since no finite witness can be used as proof.
Several forms of liveness are recognized. The following are defined in terms of a system with several processes that has a critical section guarded by some mutual-exclusion (mutex) device. It is assumed that all processes use the semaphore correctly; progress is defined as the completion of execution of the critical section.
According to B. Alpern, deadlock-freedom is a safety property. Alpern proposes that the states of a system can be partitioned into states in which a deadlock is present (red states) and states in which no deadlock is present (green states). The property stating that the system remains forever in green states (or, equivalently, that the system never reaches a red state) is a safety property. If one cannot distinguish between green and red states, however, the property stating that eventually one of the processes in the system will make progress is a liveness property.
The distinction between safety and liveness can be formally established through a predicate referring to time. Let some point in time be the moment from which liveness and safety properties are evaluated. In the examples below, let some process (or thread) be one for which we want to guarantee that it is deadlock-free. 
Safety: 
Example: means « is in a deadlocked state at time ».
Liveness: 
Example: means « stops waiting at time ».
Liveness(C,L) in the algorithm Paxos — If a decision C has been proposed, then sooner or later some process L will adopt a decision (provided a sufficient number of participating processes remain operational).
It is also worth noting that the distinction between the liveness property of bounded bypass and the safety property of bounded overtaking is a subtle one. Starvation freedom with bounded overtaking implies bounded bypass (i.e., even though bounded bypass is classified as a liveness property, it actually represents a mixture of a liveness property and a safety property). Bounded overtaking means that, after a marked process declares its interest in leaving the critical section, every other process will overtake the marked process a bounded number of times before the marked process enters the critical section. Note that if the marked process never receives permission to enter the critical section, bounded overtaking may still hold. Thus, bounded overtaking by itself is not a liveness property. In a deadlocked system, bounded overtaking is trivially satisfied, since no process overtakes another, but bounded bypass is not.
Many applications, probably most, require objects to persist from one session to the next. The environment must provide a mechanism for doing this in a simple way.
An object often contains references to other objects, which in turn also contain references to objects. Therefore, each object may have a large number of dependent objects, with a possibly complex dependency graph (which may contain cycles). It usually makes no sense to save or restore an object without all of its direct and indirect dependent objects. A persistence mechanism is said to support a persistence closure if it can automatically save the dependent objects together with the object itself.
There must exist a storage mechanism that supports persistence closure. It saves the object together with all its dependent objects on external devices and restores them within the same session or a different one.
For some applications, simple persistence support is not enough; such applications need full database support (database support) . The concept of an OO database is explained in one of the following lectures, where other persistence-related issues are also examined, such as schema evolution, the ability to safely restore objects even when the corresponding classes have changed.
Robustness is the ability of software to react appropriately to abnormal situations.
Robustness complements correctness. Correctness relates to the behavior of the system in cases defined by the specification; robustness characterizes what happens outside that specification.
Fig. 1.3. Robustness versus correctness
As is clear from the definition, robustness is, by its nature, a fuzzier notion than correctness. It is impossible to say, as we can for correctness, that in abnormal situations the system must "perform its tasks", since such situations lie outside the specification. If these tasks were known, the abnormal case would become part of the specification, and we would once again be back in the realm of correctness.
| We will need this definition of an "abnormal situation" when we study exception handling (on exceptional situations, see Lecture 12). It implies that the notions of a normal and an abnormal situation are always relative to a given specification; a situation is abnormal if it falls outside the specification. If the specification is extended, abnormal cases become normal - even if they correspond to such undesirable events as, for example, erroneous user input. |
The term "normal" in this sense does not mean "desirable", but simply "planned for in the software design". Although it may at first seem paradoxical that erroneous input can be called a normal case, any other approach relies on subjective criteria and is therefore useless.
There will always be cases that the specification does not explicitly cover. The role of the robustness requirement is to ensure that, even in such cases, the system does not lead to an irreparable situation; it must issue an appropriate error message, terminate gracefully, or enter a so-called "graceful degradation" mode.
In computer science , persistence refers to the characteristic of state that outlives the process that created it. This is achieved in practice by storing the state as data in a computer data store . Programs must transfer data to and from storage devices and must provide a mapping from the data structures native to the programming language to the data structures of the storage devices.
Image-editing programs or word processors, for example, achieve a persistent state by saving their documents to files .
Persistence is called « orthogonal » or «transparent» , when it is implemented as an intrinsic property of the program's runtime environment. An orthogonally persistent environment does not require any specific action on the part of the programs running within it , in order to obtain or save their state .
Non-orthogonal persistence requires data to be written to and read from storage using special instructions within the program, resulting in the use of save as a transitive verb: upon completion, the program saves the data .
The advantage of orthogonal persistence environments is that programs are simpler and less prone to errors.
Orthogonal persistence is widely used in operating systems for hibernation and in platform virtualization systems , such as VMware and VirtualBox , for state saving.
Prototype research languages , such as PS-algol , Napier88 , Fibonacci and pJama, have successfully demonstrated the concept along with its benefits for programmers.
System image
Using system images is the simplest persistence strategy. A laptop's sleep mode is an example of orthogonal persistence using a system image , since it requires no action on the part of the programs running on the machine. An example of non-orthogonal persistence using a system image is a simple text-editing program executing specific instructions to save the entire document to a file.
Disadvantages : It requires sufficient RAM to store the entire state of the system. State changes made to the system after the last image save are lost in the event of a system crash or power loss. Saving an image for every change would take too much time for most systems, so images are not used as the sole persistence method for critical systems.
Using logs is the second-simplest persistence method. Logging is the process of storing events in a log before each of them is applied to the system. Such logs are called journals.
At startup, the log is read and each event is reapplied to the system, avoiding data loss in the event of a system crash or power loss.
The entire «Undo / Redo» history of user commands in an image-editing program, for example, when written to a file, constitutes a log capable of restoring the state of the image being edited at any point in time.
Logs are used by journaling file systems , distributed systems and database management systems , where they are also called «transaction logs» or «redo logs».
DISADVANTAGES : Logs are often combined with other persistence methods so that the entire (potentially large) history of all system events does not have to be replayed at system startup.
This method consists of writing out only those parts of the system state that have been modified (that are dirty) since they were last written. Sophisticated document-editing applications, for example, use dirty write operations to save only the parts of the document that have actually changed since the last save.
Disadvantages: This method requires state changes to be intercepted within the program. This is achieved either in a non-transparent way, requiring specific calls to a storage API, or in a transparent way, through automatic transformation of the program . This results in code that runs slower than machine code and is harder to debug.
Any software layer that makes it easier for a program to save its state is generally called a persistence layer. Most persistence layers do not achieve persistence directly, but instead rely on an underlying database management system .
System prevalence is a method that combines the system images and operation logs mentioned above, in order to overcome their limitations.
Disadvantages: a prevalent system must have enough RAM to hold the entire state of the system.
A DBMS uses a combination of dirty write operations and the journaled transaction methods mentioned above. They provide not only persistence, but also other services, such as querying, auditing, and access control.
Persistent operating systems are operating systems that remain persistent even after a crash or an unexpected shutdown. Operating systems that make use of this capability include
What is a program? It is any piece of code that can be considered on its own. Suppose we need to write a browser. We carry out three tasks: we design the program's representation for the user, then we write a high-level outline of the program, and finally we write the code. As we write the code, we realize that we need to write a text-formatting tool. Here again we need to solve three tasks: decide what text this tool will return; choose an algorithm for the formatting; write the code. This task has its own subtask: correctly hyphenating words. We solve this subtask in three steps as well — as we can see, they recur at many levels.
Let us look more closely at the first step: what task the program solves. Here we most often model the program as a function that takes some input and produces some output. In mathematics, a function is usually described as an ordered set of pairs. For example, the squaring function on the natural numbers is described as the set {<0,0>, <1,1>, <2,4>, <3,9>, ...}. The domain of such a function is the set of the first elements of each pair, that is, the natural numbers. To define a function, we need to specify its domain and its formula.
But functions in mathematics — are not the same thing as functions in programming languages. Mathematics is significantly simpler. Since I don't have time for complex examples, let's look at a simple one: a function in C or a static method in Java that returns the greatest common divisor of two integers. In the specification of this method we would write: computes GCD(M,N) for arguments M and N, where GCD(M,N) — is a function whose domain — is the set of pairs of integers, and whose return value — is the largest integer that divides both M and N. How does this model relate to reality? The model operates on integers, whereas in C or Java we have a 32-bit int. This model lets us decide whether the GCD algorithm is correct, but it will not prevent overflow errors. That would require a more complex model, for which there is no time.
Let's talk about the limitations of a function as a model. The operation of some programs (operating systems, for example) does not reduce to returning a particular value for particular arguments; they may run continuously. Moreover, a function as a model is poorly suited to the second step: planning the way a task will be solved. Quicksort and bubble sort compute the same function, but they are completely different algorithms. Therefore, to describe the way a program achieves its goal, I use a different model, which we will call the standard behavioral model. In this model, a program is represented as the set of all admissible behaviors, each of which, in turn, is a sequence of states, and a state — is an assignment of values to variables.
Let's look at what the second step for Euclid's algorithm would look like. We need to compute GCD(M, N). We initialize M as x and N as y, then repeatedly subtract the smaller of these variables from the larger until they are equal. For example, if M = 12 and N = 18, we can describe the following behavior:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
And what if M = 0 and N = 0? Zero is divisible by every number, so in this case there is no greatest divisor. In this situation we need to go back to the first step and ask: do we really need to compute the GCD for non-positive numbers? If that's not necessary, then we should simply change the specification.
Here it's worth a brief digression about productivity. It is often measured by the number of lines of code written per day. But your work is far more useful if you got rid of a certain number of lines, because you now have less room for bugs. And getting rid of code is easiest right at the first step. It's quite possible that you simply don't need all the bells and whistles you're trying to implement. The fastest way to simplify a program and save time — is not to do things that aren't worth doing. The second step — is second in its potential for saving time. If you measure productivity by the number of lines written, then thinking through a way of accomplishing the task will make you less productive, since you'll be able to solve the same task with a smaller amount of code. I can't give you exact statistics here, since I have no way to count the number of lines I didn't write thanks to spending time on the specification, that is, on the first and second steps. And you can't set up an experiment for this either, because in an experiment we're not allowed to perform the first step — the task is defined in advance.
Informal specifications easily miss a lot of difficulties. There's nothing hard about writing rigorous specifications for functions, so I won't discuss that here. Instead we'll talk about writing rigorous specifications for standard behavioral models. There's a theorem stating that any set of behaviors can be described using the safety property (safety) and the liveness property (liveness). Safety means that nothing bad will happen — the program won't produce a wrong answer. Liveness means that sooner or later something good will happen, i.e., the program will sooner or later give a correct answer. As a rule, safety is the more important property, since errors most often occur there. So, to save time, I won't talk about liveness, although it is, of course, important too.
We achieve safety by specifying, first, the set of possible initial states. And, second, the relation to all possible next states for each state. Let's act like scientists and define the states mathematically. The set of initial states is described by a formula, for example, in the case of Euclid's algorithm: (x = M) ∧ (y = N). For given values of M and N there is only one initial state. The next-state relation is described by a formula in which the variables of the next state are written primed, and those of the current state — unprimed. In the case of Euclid's algorithm we're dealing with a disjunction of two formulas, in one of which x is the larger value, and in the other — y:
In the first case, the new value of y is equal to the previous value of y, and we obtain the new value of x by subtracting the smaller variable from the larger one. In the second case, we do the opposite.
Let's go back to Euclid's algorithm. Suppose again that M = 12, N = 18. This determines a single initial state, (x = 12) ∧ (y = 18). We then substitute these values into the formula above and get:
Here the only possible solution is: x' = 18 - 12 ∧ y' = 12, and we get the behavior: [x = 12, y = 18]. In just the same way we can describe all the states in our behavior: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
In the last state [x = 6, y = 6], both parts of the expression are false, so it has no next state. So, we have a complete specification of the second step — as you can see, this is quite ordinary mathematics, the kind used by engineers and scientists, not the strange kind found in computer science.
These two formulas can be combined into a single temporal logic formula. It's elegant and not hard to explain, but there's no time for it right now. We would only need temporal logic for the liveness property; it's not needed for safety. I don't particularly like temporal logic as such — it's not quite ordinary mathematics — but in the case of liveness it is a necessary evil.
In Euclid's algorithm, for every value of x and y there are unique values of x' and y' that make the next-state relation true. In other words, Euclid's algorithm is deterministic. To model a nondeterministic algorithm, the current state needs to have several possible future states, and each value of the unprimed variable needs to have several values of the primed variable for which the next-state relation is true. This isn't hard to do, but I won't give examples right now.
To build a working tool, you need formal mathematics. How do you make a specification formal? For that we need a formal language, for example, TLA+. The specification of Euclid's algorithm in this language would look as follows:
The equals sign with a triangle means that the value on the left of the sign is defined to be equal to the value on the right of the sign. In essence, a specification — is a definition, in our case two definitions. To the specification in TLA+ we need to add declarations and some syntax, as shown on the slide above. In ASCII it would look like this:
As you can see, nothing complicated. A TLA+ specification can be checked, i.e., all possible behaviors can be explored in a small model. In our case this model would be given values of M and N. This is a very effective and simple way of checking, and it runs entirely automatically. In addition, you can write formal proofs of correctness and check them mechanically, but that takes a lot of time, so almost nobody does it.
The main drawback of TLA+ is that it's mathematics, and programmers and computer scientists are afraid of mathematics. At first this sounds like a joke, but unfortunately I'm saying it in complete seriousness. A colleague of mine was just telling me how he tried to explain TLA+ to several developers. As soon as formulas appeared on the screen, their eyes immediately glazed over. So if TLA+ is intimidating, you can use PlusCal, which is a kind of toy programming language. An expression in PlusCal can be any TLA+ expression, that is, essentially, any mathematical expression. In addition, PlusCal has syntax for nondeterministic algorithms. Because any TLA+ expression can be written in PlusCal, it is significantly more expressive than any real programming language. Furthermore, PlusCal compiles into an easily readable TLA+ specification. This doesn't mean, of course, that a complex PlusCal specification turns into a simple one in TLA+ — it just means the correspondence between them is obvious, and no extra complexity appears. Finally, this specification can then be checked with TLA+ tools. In general, PlusCal can help overcome the fear of mathematics; it's easy to understand even for programmers and computer scientists. In the past, for a while (about 10 years) I published algorithms in it.
Someone might object that TLA+ and PlusCal — are mathematics, and mathematics only works on made-up examples. In practice you need a real language with types, procedures, objects, and so on. That's not true. Here's what Chris Newcombe, who worked at Amazon, writes: «We have used TLA+ on ten large projects, and in every case its use contributed significantly to the development, because we were able to catch dangerous bugs before they reached production, and because it gave us the understanding and confidence needed for aggressive performance optimizations that don't affect the correctness of the program». You often hear that using formal methods gives you inefficient code — in practice it's exactly the opposite. There's also a belief that managers can't be convinced of the need for formal methods even when programmers are convinced of their usefulness. But Newcombe writes: «Managers are now actively pushing for specifications to be written in TLA+, and are specifically setting aside time for it». So when managers see that TLA+ works, they gladly adopt it. Chris Newcombe wrote this about six months ago (in October 2014), and now, as far as I know, TLA+ is used in 14 projects, not 10. Another example concerns the design of the Xbox 360. An intern came to Charles Thacker and wrote a specification for the memory system. Thanks to this specification, a bug was found that would otherwise have gone unnoticed, one that would have caused every Xbox 360 to crash after four hours of use. Engineers at IBM confirmed that their tests would not have found this bug.
You can read more about TLA+ online, and now let's talk about informal specifications. We rarely have to write programs that compute the greatest common divisor and the like. Much more often we write programs like the pretty-printing tool I wrote for TLA+. After the simplest processing, TLA+ code would look like this:
But in the example given, the user most likely wanted the conjunction and equals signs to be aligned. So the correct formatting would look more like this:
Let's look at another example:
Here, on the contrary, the alignment of the equals, plus, and multiplication signs in the source was accidental, so the simplest processing is quite enough. In general, there is no precise mathematical definition of correct formatting, because «correct» here means «whatever the user wants», and that can't be defined mathematically.
You might think that if we have no definition of correctness, then a specification is useless. But that's not so. If we don't know exactly what the program should do, that doesn't mean we don't need to think through its behavior — on the contrary, we need to spend even more effort on it. A specification is especially important here. It's impossible to define the optimal program for pretty-printing, but that doesn't mean we shouldn't take it on at all and just write code as a stream of consciousness — that won't do. In the end I wrote a specification of six rules with definitions in the form of comments in a Java file. Here's an example of one of the rules: a left-comment token is LeftComment aligned with its covering token. This rule is written in, let's say, mathematical English: LeftComment aligned, left-comment, and covering token — are terms with definitions. This is how mathematicians describe mathematics: they write definitions of terms and, based on them — rules. The benefit of such a specification is that understanding and debugging six rules is much easier than debugging 850 lines of code. I should say that writing these rules wasn't easy, and quite a lot of time went into debugging them. Specifically for this purpose I wrote code that reported which rule was being used. Because I checked these six rules against several examples, I didn't need to debug 850 lines of code, and the bugs turned out to be fairly easy to find. Java has excellent tools for this. If I had just written the code, it would have taken me significantly longer, and the formatting would have come out worse.
Why couldn't a formal specification be used? On the one hand, correctness of execution isn't all that important here. Pretty-printing is bound to displease someone, so I didn't need to achieve correct behavior in every unusual situation. Even more important is the fact that I didn't have adequate tools. The TLA+ model checker is useless here, so I would have had to write the examples by hand.
The specification given has features common to all specifications. It's at a higher level than the code. It can be implemented in any language. No tools or methods are of any use in writing it. No programming course will help you write this specification. And there are no tools that could make this specification unnecessary, unless, of course, you're writing a language specifically for writing pretty-printing programs in TLA+. Finally, this specification says nothing about how exactly we're going to write the code — it only states what the code does. We write a specification to help us think through the problem before we start thinking about the code.
But this specification also has features that set it apart from other specifications. 95% of other specifications are much shorter and simpler:
Furthermore, this specification is a set of rules. As a rule, that's a sign of a bad specification. It's quite hard to understand the consequences of a set of rules, and that's exactly why I had to spend a lot of time debugging them. Nevertheless, in this case I couldn't find a better way.
It's worth saying a few words about programs that run continuously. As a rule, they run in parallel, for example, operating systems or distributed systems. Very few people can reason about them in their head or on paper, and I'm not one of them, although at one time I was capable of it. That's why we need tools that will check our work — for example, TLA+ or PlusCal.
Why did I need to write a specification if I already knew what the code should do? In reality, I only thought I knew that. Besides, with a specification in hand, an outsider no longer needs to dig into the code to understand what exactly it does. I have a rule: there should be no general rules. This rule, of course, has an exception, and it's the one general rule I follow: a specification of what the code does should tell people everything they need to know when using this code.
So, what exactly do programmers need to know about thinking? To begin with, the same thing everyone does: if you're not writing, you only think you're thinking. Also, you need to think before you code, which means you need to write before you code. A specification — is what we write before we start coding. A specification is needed for any code that might be used or modified by someone else. And that «someone else» may turn out to be the very author of the code, a month after writing it. A specification is needed for large programs and systems, for classes, for methods, and sometimes even for complicated parts of a single method. What exactly should you write about the code? You need to describe what it does, that is, whatever might be useful to anyone using this code. Sometimes it may also be necessary to specify how exactly the code achieves its goal. If we covered this method in an algorithms course, we call it an algorithm. If it's something more specialized and new, we call it high-level design. There's no formal difference here: both are an abstract model of the program.
How exactly should you write a specification for code? The main thing: it should be one level above the code itself. It should describe states and behaviors. It should be as rigorous as the task requires. If you're writing a specification of a way to implement a task, you can write it in pseudocode or with PlusCal. You need to learn to write specifications by writing formal specifications. This will give you the skills you need, which will also help with informal ones. And how do you learn to write formal specifications? When we learned to program, we wrote programs and then debugged them. It's the same here: you need to write a specification, check it with a model checker, and fix the errors. TLA+ might not be the best language for formal specification, and for your specific needs another language is probably a better fit. The advantage of TLA+ is that it teaches mathematical thinking extremely well.
How do you connect the specification and the code? Through comments that link mathematical concepts to their implementation. If you're working with graphs, then at the program level you'll have arrays of nodes and arrays of edges. So you need to write how exactly the graph is implemented by these programming structures.
It should be noted that none of the above applies to the actual process of writing code. When you're writing code, that is, performing the third step, you also need to think and reason about the program. If a subtask turns out to be complex or non-obvious, you need to write a specification for it. But I'm not talking about the code itself here. You can use any programming language, any methodology — that's not what this is about. Also, none of the above removes the need to test and debug the code. Even if the abstract model is written correctly, there can still be bugs in its implementation.
Writing specifications — is an extra stage in the process of writing code. Thanks to it, many errors can be caught with less effort — we know this from the experience of programmers at Amazon. With specifications, the quality of programs goes up. So why then do we so often skip them? Because writing is hard. And writing is hard because it requires thinking, and thinking is also hard. It's always easier to just pretend you're thinking. You can draw an analogy here with running — the less you run, the slower you run. You need to train your muscles and practice writing. It takes practice.
A specification can be wrong. You might have made a mistake somewhere, or the requirements might have changed, or an improvement turned out to be necessary. Any code that anyone uses eventually has to be changed, so sooner or later the specification will stop matching the program. Ideally, in that case you should write a new specification and completely rewrite the code. We know perfectly well that nobody does that. In practice we patch the code and, perhaps, update the specification. If that's bound to happen sooner or later anyway, then why write specifications at all? First, for the person who will be fixing your code, every extra word in the specification is worth its weight in gold, and that person could very well be you yourself. I often scold myself for an insufficient specification when I'm fixing my own code. And I write more specifications than code. So, whenever you fix code, you should always update the specification. Second, with every fix the code gets worse, becoming harder and harder to read and maintain. This is the buildup of entropy. But if you don't start with a specification, then every line you write will be a fix, and the code will be unwieldy and hard to read from the very start.
As Eisenhower said, no battle was ever won according to plan, and no battle was ever won without one. And he knew a thing or two about battles. There's a view that writing specifications — is a waste of time. Sometimes that's really true, and the task is so simple there's nothing to think through. But you should always remember that when someone advises you not to write specifications, what they're really advising you is not to think. And that's worth thinking about every time. Thinking a task through doesn't guarantee you won't make mistakes. As we know, nobody has invented a magic wand, and programming — is a hard business. But if you don't think the task through, you are guaranteed to make mistakes.
1 The ResiliNets Research Initiative definition of survivability.
2 Abdul Jabbar Mohammad, David Hutchison, and James P.G. Sterbenz "Poster: Towards Quantifying Metrics for Resilient and Survivable Networks", 14th IEEE International Conference on Network Protocols (ICNP 2006), Santa Barbara, California, USA, November 2006
3 Balzer, Stephanie (November 17, 2005). «Contract Programming Persistent Objects» (PDF) . University of Glasgow - School of Computing Science - Research . ETH Zürich
4. Popkov, V. K. Mathematical Models of Communication Network Survivability. – Novosibirsk: Siberian Branch of the USSR Academy of Sciences. 1990. –235 p.
5. Cherkesov, G. N. Methods and Models for Assessing the Survivability of Complex Systems. — Moscow: Znanie, —1987. —55 p.
6. Netes, V.A. Reliability of Communication Networks in the Transition to NGN. Moscow: – Vestnik Svyazi, No. 9. 2007. – pp. 4-5
7. DSTU B3265 – 95 Military Communications. Terms and Definitions. Effective from 1997–01–01. State Standard of Ukraine, p.23
8 Stanford Seminar - Programing Should Be More Than Coding https://youtu be.com/watch?v=6QsTfL-uXd8
Comments