This article is a translation . But before her a little introduction. How are zombies formed? Everyone got into a situation where they want to pull a friend or colleague up to their level, but it doesn’t work out. And it’s not so much with you as with him that “it doesn’t work out”: on one side of the scale is a normal salary, tasks, and so on, and on the other, the need to think. Thinking is unpleasant and painful. He quickly gives up and continues to write code without turning on his brain at all. You imagine how much effort it takes to overcome the barrier of learned helplessness, and you just don't do it. This is how zombies are formed, which, it seems, can be cured, but it seems that no one will do it.
When I saw that (yes, the same comrade from the textbooks) and does not make a report, but a question-and-answer session, I was a little wary. Just in case, Leslie is a world-famous scientist, the author of fundamental works in distributed computing, and you can also know him by the letters La in the word LaTeX - “Lamport TeX”. The second alarming factor is his requirement: everyone who comes must (absolutely free of charge) listen to a couple of his reports in advance, come up with at least one question on them, and only then come. I decided to see what Lamport was broadcasting there - and it's great! It's exactly that thing, the magic link-pill to cure zombies. I warn you: from the text, lovers of super-flexible methodologies and those who do not like to test what is written can notably burn out.
After habrokat, in fact, the translation of the seminar begins. Enjoy reading!
Whatever task you take on, you always need to go through three steps:
- decide what goal you want to achieve;
- decide how you will achieve your goal;
- come to your goal.
This also applies to programming. When we write code, we need to:
- decide what the program should do;
- determine how it should perform its task;
- write the corresponding code.
The last step, of course, is very important, but I will not talk about it today. Instead, we will discuss the first two. Every programmer performs them before starting to work. You don't sit down to write unless you've decided whether you're writing a browser or a database. A certain idea of the goal must be present. And you definitely think over what exactly the program will do, and do not write somehow in the hope that the code will somehow turn into a browser.
How exactly does this code pre-thinking happen? How much effort should we put into this? It all depends on how complex the problem we are solving. Suppose we want to write a fault-tolerant distributed system. In this case, we should think things over carefully before we sit down to code. What if we just need to increment an integer variable by 1? At first glance, everything is trivial here, and no thought is needed, but then we remember that an overflow can occur. Therefore, even in order to understand whether a problem is simple or complex, you first need to think.
If you think about possible solutions to the problem in advance, you can avoid mistakes. But this requires that your thinking be clear. To achieve this, you need to write down your thoughts. I really like the Dick Guindon quote: “When you write, nature shows you how sloppy your thinking is.” If you do not write, you only think that you are thinking. And you need to write down your thoughts in the form of specifications.
Specifications perform many functions, especially in large projects. But I will only talk about one of them: they help us think clearly. Thinking clearly is very important and quite difficult, so here we need any help. What language should we write specifications in? In general, this is always the first question for programmers: what language will we write in. There is no one correct answer to it: the problems we are solving are too diverse. For some, TLA+ is a specification language that I developed. For others, it is more convenient to use Chinese. Everything depends on the situation.
More important is another question: how to achieve clearer thinking? Answer: We must think like scientists. This is a way of thinking that has proven itself over the past 500 years. In science, we build mathematical models of reality. Astronomy was perhaps the first science in the strict sense of the word. In the mathematical model used in astronomy, celestial bodies appear as points with mass, position and momentum, although in reality they are extremely complex objects with mountains and oceans, tides and tides. This model, like any other, was created to solve certain problems. It is great for determining where to point the telescope if you need to find a planet. But if you want to predict the weather on this planet, this model won't work.
Mathematics allows us to determine the properties of the model. And science shows how these properties relate to reality. Let's talk about our science, computer science. The reality with which we work is computing systems of various kinds: processors, game consoles, computers, executing programs, and so on. I will talk about running a program on a computer, but by and large, all these conclusions apply to any computing system. In our science, we use many different models: the Turing machine, partially ordered sets of events, and many others.
What is a program? This is any code that can be considered independently. Suppose we need to write a browser. We perform three tasks: we design the user's view of the program, then we write the high-level diagram of the program, and finally we write the code. As we write the code, we realize that we need to write a text formatter. Here we again need to solve three problems: determine what text this tool will return; select an algorithm for formatting; write code. This task has its own subtask: correctly insert a hyphen into words. We also solve this subtask in three steps - as you can see, they are repeated at many levels.
Let's consider in more detail the first step: what problem the program solves. Here, we most often model a 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 for 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 scope and formula.
But functions in mathematics are not the same as functions in programming languages. The math is much easier. Since I don't have time for complex examples, let's consider 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 will write: calculates GCD(M,N) for arguments M и NWhere GCD(M,N) - a function whose domain is the set of pairs of integers, and the return value is the largest integer that is divisible by M и N. How does this model relate to reality? The model operates on integers, while in C or Java we have a 32-bit int. This model allows us to decide if the algorithm is correct GCD, but it won't prevent overflow errors. This would require a more complex model, for which there is no time.
Let's talk about the limitations of a function as a model. Some programs (such as operating systems) don't just return a certain value for certain arguments, they can run continuously. In addition, the function as a model is not well suited for the second step: planning how to solve the problem. Quick sort and bubble sort compute the same function, but they are completely different algorithms. Therefore, to describe how the goal of the program is achieved, I use a different model, let's call it the standard behavioral model. The program in it is represented as a set of all permissible behaviors, each of which, in turn, is a sequence of states, and the state is the assignment of values to variables.
Let's see what the second step for the Euclid algorithm would look like. We need to calculate GCD(M, N). We initialize M How x, N How y, then repeatedly subtract the smaller of these variables from the larger until they are equal. For example, if M = 12, N = 18, we can describe the following behavior:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
And if the M = 0 и N = 0? Zero is divisible by all numbers, so there is no greatest divisor in this case. In this situation, we need to go back to the first step and ask: do we really need to calculate GCD for non-positive numbers? If this is not necessary, then you just need to change the specification.
Here we should make a small digression about productivity. It is often measured in the number of lines of code written per day. But your work is much more useful if you get rid of a certain number of lines, because you have less room for bugs. And the easiest way to get rid of the code is at the first step. It's entirely possible that you just don't need all the bells and whistles you're trying to implement. The fastest way to simplify a program and save time is to not do things that shouldn't be done. The second step is the second most time-saving potential. If you measure productivity in terms of lines written, then thinking about how to accomplish a task will make you less productive, because you can solve the same problem with less code. I can’t give exact statistics here, because I have no way to count the number of lines that I didn’t write due to the fact that I spent time on the specification, that is, on the first and second steps. And the experiment cannot be set up here either, because in the experiment we do not have the right to complete the first step, the task is predetermined.
It is easy to overlook many difficulties in informal specifications. There is nothing difficult in writing strict specifications for functions, I will not discuss this. Instead, we'll talk about writing strong specifications for standard behaviors. There is a theorem that says that any set of behaviors can be described using the security property (safety) and survivability properties (liveness). Security means that nothing bad will happen, the program will not give an incorrect answer. Survivability means that sooner or later something good will happen, i.e. the program will give the correct answer sooner or later. As a rule, security is a more important indicator, errors most often occur here. Therefore, to save time, I will not talk about survivability, although it is, of course, also important.
We achieve security by prescribing, first, the set of possible initial states. And second, relationships with all possible next states for each state. Let's act like scientists and define states mathematically. The set of initial states is described by a formula, for example, in the case of the Euclid algorithm: (x = M) ∧ (y = N). For certain values M и N there is only one initial state. The relationship with the next state is described by a formula in which the variables of the next state are written with a prime, and the variables of the current state are written without a prime. In the case of Euclid's algorithm, we will deal with the disjunction of two formulas, in one of which x is the largest value, and in the second - y:
In the first case, the new value of y is equal to the previous value of y, and we get 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. Let's assume again that M = 12, N = 18. This defines a single initial state, (x = 12) ∧ (y = 18). We then plug those values into the formula above and get:
Here's the only possible solution: x' = 18 - 12 ∧ y' = 12and we get the behavior: [x = 12, y = 18]. Similarly, we can describe all the states in our behavior: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
In last state [x = 6, y = 6] both parts of the expression will be 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, like in engineers and scientists, and not strange, like in computer science.
These two formulas can be combined into one formula of temporal logic. She is elegant and easy to explain, but there is no time for her now. We may need temporal logic only for the liveliness property, it is not needed for security. I don't like temporal logic as such, it's not quite ordinary mathematics, but in the case of liveliness it is a necessary evil.
In Euclid's algorithm, for each value x и y have unique values x' и y', which make the relation with the next state true. In other words, Euclid's algorithm is deterministic. To model a non-deterministic algorithm, the current state needs to have multiple possible future states, and that each unprimed variable value has multiple primed variable values such that the relation to the next state is true. This is easy to do, but I won't give examples now.
To make a working tool, you need formal mathematics. How to make the specification formal? To do this, we need a formal language, for example, . The specification of the Euclid algorithm would look like this in this language:
An equal sign symbol with a triangle means that the value to the left of the sign is defined to be equal to the value to the right of the sign. In essence, the specification is a definition, in our case two definitions. To the specification in TLA+, you need to add declarations and some syntax, as in the slide above. In ASCII it would look like this:
As you can see, nothing complicated. The specification for TLA+ can be tested, i.e. bypass all possible behaviors in a small model. In our case, this model will be certain values M и N. This is a very efficient and simple verification method that is completely automatic. It is also possible to write formal truth proofs and check them mechanically, but this takes a lot of time, so almost no one does this.
The main disadvantage of TLA+ is that it is math, and programmers and computer scientists are afraid of math. At first glance, this sounds like a joke, but, unfortunately, I mean it in all seriousness. My colleague was just telling me how he tried to explain TLA+ to several developers. As soon as the formulas appeared on the screen, they immediately became glassy eyes. So if TLA+ scares you, you can use , it's kind of a toy programming language. An expression in PlusCal can be any TLA+ expression, that is, by and large, any mathematical expression. In addition, PlusCal has a syntax for non-deterministic algorithms. Because PlusCal can write any TLA+ expression, PlusCal is much more expressive than any real programming language. Next, PlusCal is compiled into an easily readable TLA+ specification. This does not mean, of course, that the complex PlusCal specification will turn into a simple one on TLA + - just the correspondence between them is obvious, there will be no additional complexity. Finally, this specification can be verified by TLA+ tools. All in all, PlusCal can help overcome math phobia and is easy to understand even for programmers and computer scientists. In the past, I published algorithms on it for some time (about 10 years).
Perhaps someone will object that TLA + and PlusCal are mathematics, and mathematics only works on invented examples. In practice, you need a real language with types, procedures, objects, and so on. This is wrong. Here is what Chris Newcomb, who worked at Amazon, writes: “We've used TLA+ on ten major projects, and in each case, using it has made a significant difference to development because we were able to catch dangerous bugs before we hit production, and because it gave us the insight and confidence we needed to make aggressive performance optimizations without affecting the truth of the program". You can often hear that when using formal methods, we get inefficient code - in practice, everything is exactly the opposite. In addition, there is an opinion that managers cannot be convinced of the need for formal methods, even if programmers are convinced of their usefulness. And Newcomb writes: “Managers are now pushing hard to write specifications for TLA +, and specifically allocate time for this”. So when managers see that TLA+ is working, they are happy to accept it. Chris Newcomb wrote this about six months ago (October 2014), but now, as far as I know, TLA+ is used in 14 projects, not 10. Another example is in the design of the XBox 360. An intern came to Charles Thacker and wrote specification for the memory system. Thanks to this specification, a bug was found that would otherwise go unnoticed, and because of which every XBox 360 would crash after four hours of use. IBM engineers confirmed that their tests would not have found this bug.
You can read more about TLA + on the Internet, but now let's talk about informal specifications. We rarely have to write programs that calculate the least common divisor and the like. A lot more often we write programs like the pretty-printer tool I wrote for TLA+. After the simplest processing, the TLA + code would look like this:
But in the above example, the user most likely wanted the conjunction and equal signs to be aligned. So the correct formatting would look more like this:
Let's consider another example:
Here, on the contrary, the alignment of the equals, addition, and multiplication signs in the source was random, so the simplest processing is quite enough. In general, there is no exact mathematical definition of correct formatting, because "correct" in this case means "what the user wants", and this cannot be mathematically determined.
It would seem that if we do not have a definition of truth, then the specification is useless. But it's not. Just because we don't know what a program is supposed to do doesn't mean we don't need to think about how it works—on the contrary, we have to put even more effort into it. The specification is especially important here. It is impossible to determine the optimal program for structured printing, but this does not mean that we should not take it at all, and writing code as a stream of consciousness is not a good thing. In the end, I wrote a specification of six rules with definitions in the form of comments in a java file. Here is an example of one of the rules: a left-comment token is LeftComment aligned with its covering token. This rule is written in, shall we say, mathematical English: LeftComment aligned, left-comment и covering token - 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 six rules are much easier to understand and debug than 850 lines of code. I must say that writing these rules was not easy, it took quite a lot of time to debug them. Especially for this purpose, I wrote a code that reported which rule was used. Thanks to the fact that I tested these six rules on several examples, I did not have to debug 850 lines of code, and bugs turned out to be quite easy to find. Java has great tools for this. If I had just written the code, it would have taken me much longer, and the formatting would have been of poorer quality.
Why couldn't a formal specification be used? On the one hand, the correct execution is not too important here. Structural printouts are bound to not please anyone, so I didn't have to get it to work right in all the odd situations. Even more important is the fact that I didn't have adequate tools. The TLA+ model checker is useless here, so I would have to manually write the examples.
The above specification has features common to all specifications. It is higher level than the code. It can be implemented in any language. Any tools or methods are useless for 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 are writing a language specifically for writing structured print programs in TLA+. Finally, this specification doesn't say anything about exactly how we will write the code, it only states what this code does. We write the specification to help us think through the problem before we start thinking about the code.
But this specification also has features that distinguish it from other specifications. 95% of other specs are significantly shorter and simpler:
Further, this specification is a set of rules. As a rule, this is a sign of poor specification. Understanding the consequences of a set of rules is quite difficult, which is why I had to spend a lot of time debugging them. However, in this case, I could not find a better way.
It is worth saying a few words about programs that run continuously. As a rule, they work in parallel, for example, operating systems or distributed systems. Very few people can understand them mentally or on paper, and I am not one of them, although I once was able to do it. Therefore, we need tools that will check our work - for example, TLA + or PlusCal.
Why was it necessary to write a specification if I already knew what exactly the code should do? In fact, I just thought I knew it. In addition, with a specification, an outsider no longer needs to get into the code to understand what exactly he does. I have a rule: there should be no general rules. There is an exception to this rule, of course, it's the only general rule I follow: the specification of what the code does should tell people everything they need to know when using the code.
So what exactly do programmers need to know about thinking? For starters, the same as everyone else: if you do not write, then it only seems to you that you are thinking. Also, you need to think before you code, which means you need to write before you code. The specification is what we write before we start coding. A specification is needed for any code that can be used or modified by anyone. And this "someone" may be the author of the code himself a month after it was written. A specification is needed for large programs and systems, for classes, for methods, and sometimes even for complex sections of a single method. What exactly should be written about the code? You need to describe what it does, that is, what can be useful to any person using this code. Sometimes it may also be necessary to specify how the code accomplishes its purpose. If we went through this method in the course of algorithms, then we call it an algorithm. If it is something more special and new, then we call it high-level design. There is no formal difference here: both are an abstract model of a program.
How exactly should you write a code specification? The main thing: it should be one level higher than the code itself. It should describe states and behaviors. It should be as strict as the task requires. If you are writing a specification for how a task is to be implemented, you can write it in pseudocode or with PlusCal. You need to learn how to write specifications on formal specifications. This will give you the necessary skills that will help you with informal ones as well. 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: write the spec, check it with the model checker, and fix the bugs. TLA+ may not be the best language for a formal specification, and another language is likely to be better for your specific needs. The advantage of TLA+ is that it teaches mathematical thinking very well.
How to link specification and code? With the help of comments that link mathematical concepts and their implementation. If you work with graphs, then at the program level you will have arrays of nodes and arrays of links. Therefore, you need to write exactly how 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 write the code, that is, you perform the third step, you also need to think and think through 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, it's not about them. Also, none of the above eliminates the need to test and debug code. Even if the abstract model is written correctly, there may be bugs in its implementation.
Writing specifications is an additional step in the coding process. Thanks to it, many errors can be caught with less effort - we know this from the experience of programmers from Amazon. With specifications, the quality of programs becomes higher. So why, then, do we so often go without them? Because writing is hard. And writing is difficult, because for this you need to think, and thinking is also difficult. It's always easier to pretend what you think. Here you can draw an analogy with running - the less you run, the slower you run. You need to train your muscles and practice writing. Need practice.
The specification may be incorrect. You might have made a mistake somewhere, or the requirements might have changed, or an improvement might need to be made. Any code that anyone uses has to be changed, so sooner or later the specification will no longer match the program. Ideally, in this case, you need to write a new specification and completely rewrite the code. We know very well that no one does that. In practice, we patch the code and possibly update the specification. If this is bound to happen sooner or later, then why write specifications at all? Firstly, for the person who will edit your code, every extra word in the specification will be worth its weight in gold, and this person may well be you yourself. I often berate myself for not getting enough specification when I'm editing my code. And I write more specifications than code. Therefore, when you edit the code, the specification always needs to be updated. Secondly, with each revision, the code gets worse, it becomes more and more difficult to read and maintain. This is an increase in entropy. But if you don't start with a spec, then every line you write will be an edit, and the code will be unwieldy and hard to read from the start.
As said , no battle was won by plan, and no battle was won without a plan. And he knew a thing or two about battles. There is an opinion that writing specifications is a waste of time. Sometimes this is true, and the task is so simple that there is nothing to think through it. But you should always remember that when you are told not to write specifications, you are told not to think. And you should think about it every time. Thinking through the task does not guarantee that you will not make mistakes. As we know, no one invented the magic wand, and programming is a difficult task. But if you don't think through the problem, you are guaranteed to make mistakes.
You can read more about TLA + and PlusCal on a special website, you can go there from my home page . That's all for me, thank you for your attention.
Please note that this is a translation. When you write comments, remember that the author will not read them. If you really want to chat with the author, then he will be at the Hydra 2019 conference, which will be held July 11-12, 2019 in St. Petersburg. Tickets can be purchased .
Source: habr.com