Software quality/correctness (ws: UEFI question)

[PeterX]

By the way, could you tell me more about Fótism? Unfortunately I searched for it using both Startpage and DuckDuckGo (I don't use Google) and I found only one search result with Startpage: this topic. DuckDuckGo didn't return any results with Fótism (yes, I put it in quotes so it's exactly this and not something similar-looking).

Not surprising This is a local slang at my university, also called the Zen-of-Fóthi (sorry, Hungarian only). Long story short, my prof, Dr. Ákos Fóthi created a programming methodology based on mathematics in the early 1980's at ELTE. I couldn't find that book on-line (I've a printed version), but I could find a link to another book, called "Prelude to Programming" (sorry, Hungarian only). Note this book is not about the methodology, rather it's a prerequisite that explains the background, a glossary if you'd like.

That's unfortunate, I'd be interested to understand what are the main concepts of this methodology.

But how do you formally prove your code to be correct?

For example Fóthism Here's a list of things required for a master's degree, called "Theory of Programming Methodology" (again, sorry, Hungarian only). This is a non-official paper written by one of PhD students.

How does Fóthism achieve that though, if not to prove correctness as you say below, but to effectively ensure it?

Unfortunately I can't speak Magyarorzak, too. Strangely I can translate the "Zen" text to my native tongue, German, with a mouse click. I don't know if this is a feature of Chromium or of the website. And the translation is actually quite good. Unfortunately AI always tries to think for you, which leaves reasons for unsatisfaction. In this case, the AI won't allow me to translate to English.

Mathematical representation of the coding was always a bit too advanced for me. So I won't understand concepts of proving mathematically that the code is correct. (And I had specialization in Math back in school...) But maybe I can understand the Fóthi methodology.

Greetings
Peter

[bzt]

Unfortunately I can't speak Magyarorzak, too.

Nice that you've tried It is Magyarország, but that means Hungary (literally Country of the Hungarians). The language is called Magyar.

I'd be interested to understand what are the main concepts of this methodology.

Mathematical representation of the coding was always a bit too advanced for me. So I won't understand concepts of proving mathematically that the code is correct. (And I had specialization in Math back in school...) But maybe I can understand the Fóthi methodology.

Ok, I'll try to explain with simple words the basic concept. For the exact definitions and formally correct mathematical definitions please see Prelude to Programming.

TL;DR Keep in mind, that this book is not about the programming methodology per se, this is just the preface that explains elementary programming definitions using mathematics. This is the book for the first semester (so there's actually half a year to comprehend this, my post cannot be that verbose, sorry).

The first section of the book is about basic mathematical concepts. Sets, sequences (or chains? not sure about the proper translation), relations, Descartes multiplication of sets (calls it direct-multiplication), functions, things like that.

The second section is where it becames interesting, here we define three things:

State-space
Imagine that you have a Descartes multiplication of sets. Each set represents one variable (in mathematical, not programming sense, see Section 10). For example, let's say you want to repesent a point in space. For that you'll need 3 coordinates, therefore the product of C1 x C2 x C3. Each point would have one element from this (multiplied) set. So by specifying one element a from C1, b from C2, and c from C3, then a point = {a,b,c}. Hope this is clear. Note: I did not talk about the data presentation (variable in programming sense), it doesn't matter if those coordinates are actually stored as integers or floating point numbers.

Why is it called state-space? Because if you take one element for each set in it, you'll get a certain state of the machine at a given time (not a computer, just an abstract machine).

Problem
Now there's no formal specification how to define the state-space. You must include all variables that your problem depends on. You specify the problem instead that you want to solve. This looks like F (subseteq) A x A. Here subseteq means that the relation could cover the whole state-space to state-space, or could be just part of it (meaning not all states necessarily matters from the problem's point of view).

The point is, you specify that which states must lead to which states. Hope this makes sense. (Just a note, although listing all expected combination is theoretically correct, it is very combersome in practice. Section 3 will take care of that).

Program
A program is a sequence (chain) of states, where each element comes from the state-space.
A1 -> A2 -> A3 -> ...
It is important, that this sequence must be unique, well-defined and no states are allowed to be repeated. So for example if you have A2 state, then the next state must be A3, nothing else (deterministic). If Ap and Aq states can equally follow An state, then your state-space is incorrect, and probably incomplete, you need to add a new variable that you previously forgot about. If an An state repeats, that means you have an infinite loop. Only well-defined programs counts, we don't care about programs that don't have such a unique chain of states.

Now that we have clearified these, here comes the definition of the outter most importance.

Solution
When can we say that a given program solves a certain problem? This is explained in detail in section 2.5. In short, we create a function of the program, and we examine if that function leads from all input states to the expected out states. Here it is important to talk about the difference between correctness and completeness:
1. a program function is correct, if it leads from a certain state to the correct state
2. it is complete, if it's correct to all states specified by the problem, and does not assign states to states that are not included in the problem.

Hope this makes sense so far, it is not easy to digest, I know. But the good news is, this is all what strictly needed to prove if a program is formally correct. However it is extremely difficult to use these definitons to actual program code, so the rest of the book is about what to do with that.

Section 3 is about the Specification, which talks about how to describe the problem with more human-like constructs than a states to states relation. Here the key element is the "smallest prerequirement". You can only use programs in the solution that fulfill that requirement on the state-space. For example you can only use binary search on an array if the array is sorted. If the state-space contains unsorted data, then you can't use binary search. You must use a different one (which works correctly on unsorted elements), or you must insert a program before the binary search that sorts the data.

Section 4 is about how to expand a program's state-space into a another, bigger state-space (basically introduces locality, that a procedure will operate on just a few sets in the state-space product).

Section 5 is about how to expand the solution to a bigger state-space. This guarantees later that we don't have to calculate all programs at once, but instead we can split them into smaller parts specified individually. If all parts are correct and complete, then the whole is going to be correct and complete.

Sections 6-9 use Dijskra's law to simplify the program, without loosing calculatibility and correctness. Defining a program as a chain of states is very explicit, but Dijskra has proven that all algorithms can be described by using three constructs: sequence, conditional and iteration.
Here conditional is a bit tricky, because it's not like "if" in most programming languages. It's more like a very advanced "switch", or like an "if-else-if-else-if-else" construct chain. It mandates that the conditions must be disjunct (no overlap) and must cover the entire state-space. (Simply put, for a boolean expression, you always must write the program for the true branch as well as for the false branch. Like if you were forced to always use "else" in an if, or "default" in a "switch". The program in a branch can be empty (do nothing), but you must define all cases. This is important so that you can prove correctness later.)
Another difference, that simple expression "while" loops are not allowed. All iterations must be accounted for in a loop, so you must use a counter in each and every loop, and you must check for that counter in the loop's condition. It can be arbitrarly large, but you must not allow infinite loop to happen (with other words, there's always a timeout to everything). At least that's how I used to learn it, in the Third Edition that I linked, on page 76 the 6.3. definition does not contain this restriction any more, but it mentions in the description that infinite loops (case a3) should be excluded from deterministic programs.
Some simple programs are also defined, like SKIP (you would call that NOP, I'm certain, but Fóthi is not a native English speaker), ABORT, etc.

Sections 10-11 is about what those variables in the Descartes-product of state-space are. This definition allows to have another product as a type, and requires that a certain set of methods are defined to manipulate that part of the state-space. If you came from OOP, then type is similar to a class, and each variable in the cross-product is an instance. This is an extremely simplified explanation, I'm sure Fóthi would have take my head for it on an exam, but I hope you get the point. (Every class is an abstract type, but not every abstract type is a class.)
This is the abstract type (sometimes also called "intent" of the variable) that must be represented in Hungarian-notation, and not the actual data representation. This often leads to confusion. See MS blog: "One thing to keep in mind about Hungarian is that there are two totally different Hungarian implementations out there. The first one, which is the one that most people know about, is “Systems Hungarian”. System’s Hungarian is also “Hungarian-as-interpreted-by-Scott-Ludwig”. In many ways, it’s a bastardization of “real” (or Apps) Hungarian as proposed by Charles Simonyi.".

Section 12 arrives to the point that will be familiar to most of you: well-known search algorithms. It explains how to use everything we talked about so far in practice, for example describes linear search, logarithmic search, back-track search etc. This section is very useful to understand how this all works, and how the State-space/Problem/Program/Solution fits together.

Section 13 explains in great detail what transformations are allowed on the state-space to keep correctness. For example: let's say you have a problem: how long is the longest word in a text? Now you can't use the maximum-search on a state-space with characters. But if you convert that into a state-space that contains numbers (the corresponding length of each word), then you can easily use maximum-search on that set. Your solution will be correct, provided the numbers are really the lengths of the words in the original input text.

Section 14 is the lovechild of Fóthi. It is a special case of a Turing-machine that actualizes values in a set. Actually it is pretty useful, and can be used to describe operations like INSERT, DELETE and REPLACE on databases, as well as to describe allocation strategies.

Was it long?
Yes, I know. And this is just the first semeter. In the second and third semester, you can actually learn about programming methodology, that is, how to use all of this on more complex algorithms. For that, it first defines asymptotic behaviour (the O()), then it talks about many many many algorithms (you would hate having an exam, trust me). These algorithms are strictly mathematical first (like finding square root), then more complex ones come (like quick sort and Huffman-encoding, and even finding the shortest path in a graph).

The whole point of this is, that don't consider your problem as one big problem. Instead, split it into smaller parts (which going to be separate procedures probably). Use transformations on each part until you can solve a specific part with a well-known (and already proven) algorithm, so that you only have to prove your transformations were correct, which is a lot easier than proving algorithms correct. If you're lucky, then your program will be nothing more than parameterizing well-proven algorithms from a trusted library (but no, this rarely happens, there are always small parts that no previously defined algorithms cover).

Even if you don't use this methodology to prove correctness formally, this kind of thinking (abstract your problem into smaller, more handable ones) is very useful in every day coding.

Cheers,
bzt

[PeterX]

Interesting stuff. I can't understand everything immediately (of course, since this is university stuff for a semester or more). But I understand the "state-space" and the "program". I don't understand the "problem" very well.

I see a problem with this methodology when it comes to GUI programs (as purely functional languages seem to have, too) : Infinite loops, unchanged state, unpredictable input and side effects. But maybe there is a solution to that in the methodology.

Greetings
Peter

[bzt]

I don't understand the "problem" very well.

Yep, it's difficult to translate. "Feladat" can be translated as duty, exercise, to do, mission, etc. I went on with the "problem to be solved" as I thought that's the closest in this context.

For example: let's say we have a state-space of N x N, and we need to solve addition. Then we would define the problem as:

Code: Select all

In       Out
(0,0) -> (0,0)
(1,0) -> (1,0)
(1,1) -> (2,1)
(2,1) -> (3,1)
(2,2) -> (4,2)
etc.

As I've said, listing all combination is formally correct, but not practical, that's what the Section 3 with the specification is about.

I see a problem with this methodology when it comes to GUI programs (as purely functional languages seem to have, too) : Infinite loops, unchanged state, unpredictable input and side effects. But maybe there is a solution to that in the methodology.

That's just because you haven't understand the concept well. I couldn't give back a semester worth lecture in a single post, sorry. Correctness is completely indifferent to GUI and such. You're confusing abstract type to data representation (common mistake).

Infinite loops: are not part of a well-defined program chain (they never lead to the set of state-space that's defined as solution, actually they never lead to anywhere)
unchanged state: see program definition for SKIP
unpredictable input: badly defined state-space
side effects: not possible with proper state-space and well-defined programs (that's one point of correctness, to eliminate these. Also see what I wrote about completeness). Btw, there are many languages which are side effects-free (think about Ada). This means it is easier to write well-defined programs in those languages.

Oh, and one more thing: software quality != correctness. For example bubble sorting 1 million records would be correct (as it gives the expected result), but I wouldn't call that good quality (because it would take ages to run).

Cheers,
bzt

[PeterX]

I understand a bit better now (as far as it is possible so fast). To me it seems similar to purely functional programming. And it kind of invites (maybe even forces) the "programmer" (if that's the right term) to modularize "problems" into smaller problems/functions and prove them.

Greetings
Peter

[bzt]

To me it seems similar to purely functional programming.

Then you're not getting it. On page 8 it explains the relation to lambda-calculus and different programming paradigms. You can use these methodology for OOP easily (actually there's a semester where you must use it with Ada and C++, both being OOP languages. Or that's how it was in my time, I believe it's now Java and C++).

And it kind of invites (maybe even forces) the "programmer" (if that's the right term) to modularize "problems" into smaller problems/functions and prove them.

Yeah, exactly. Proving a huge program to be correct is very hard. Proving a small program to be correct is easy, and if you're building your larger program only with previously proven parts, then your entire large program will be correct. (You would do this anyway, you do use functions in C right? And classes in C++?) In an OOP language such smaller part would be a class, something that defines what you can do with a specific part of the state-space (with an instance in OOP parlance). Then you can prove a class implementation to be correct, and after that you don't have to prove it again when you use it with valid inputs only.

I'll try to explain through an example. Let's say you want to formally prove an algorithm to be correct that needs user keypress. Then you would specify a variable in the state-space which has its "smallest prerequirement" defined as a "key from the user". That's the abstract type, user key input. It doesn't matter where that value comes from, all programs can be used that fulfill that prerequirement (could be ncurses, getc(), or even a GUI event). Programs that do not return key press, can't be used, and using a program that does not fulfill one of the prerequirements would be incorrect.

As I've tried to explain, the whole point of this methodology is, to create smaller parts, let's call them units, with well-defined interfaces, and well-defined outputs for certain inputs. No inputs nor outputs are allowed that's not part of the unit's "problem to be solved" relation, to eliminate side effects or unpredictable results. Now how you implement that is out of scope: could be a feature of the language (like Ada), inputs could be checked on caller side or on the callee side. The point is, units must behave correctly for all valid inputs, and they must not given/accept invalid inputs. In general it is the best practice to check inputs if they fulfill the prerequirements in every unit. But not always, for example with binary search (which requires a sorted array), you definitely don't want to check if the input array is sorted. There you make sure of it on the caller side that only sorted arrays are given as input.

Cheers,
bzt

[testjz]

PeterX, thank you for opening this topic!

Sorry I didn't reply earlier (furthermore since this was a topic I myself asked for), but I felt the need to take a break from posting here. This break also became too stretched, because I had some busy days and, also, there are more pending replies apart from this one. So, let's go...

This is the book for the first semester (so there's actually half a year to comprehend this, my post cannot be that verbose, sorry).

Well, I never asked that! I even imagined that your post would be less verbose, but it's all good that you like teaching about various topics, specifically Fóthism in this case. Thank you too for your enlightening post!

State Spaces
I think I can relate the state space to the finite-state machine, and I think I can relate the specifying the relations of the input state to the output to both state diagrams (of any kind) and also to Carnaugh maps in binary combinatorial logic (except that there are intermediate states here if I understand the theory correctly). I think I understand it perfectly why you can have neither non-deterministic state relations, nor repeated states. In the former case, the program wouldn't be deterministic, as it would depend on things other than the state space. In the latter case, the program would have an infinite loop, as the same state would initiate the same deterministic loop again and again, infinitely. I'm however not sure whether I understand the phrase "You specify the problem instead that you want to solve", that is instead of what?

Specification
I think I can relate the specification to another concept called Design by Contract. Basically, you have preconditions that must be true when a procedure is going to be executed, side effects that the procedure will cause when executed, and also postconditions that must be true when a procedure is going to return. In any case, you also have the "class invariant" (which can be also "ported" to non-OOP structured programming), which basically means that the procedure can't cause the "class attributes" (or simply variables in non-OOP structured programming) to have a state outside of the defined state-space (to use the terminology of the methodology we talk about here).

State space expansion and solution expansion
This basically is modularity of procedures, I suppose? If so, I understand the general theory, but there are probably some more details to it.

Dijkstra's law
I think I understand it in theory. But I have a question. How do we notate conditionals that depend only on some parts of the state space (most common case in practice)? When we write an "if/else" statement, we don't put the entire state space inside the condition because that would be impractical or even impossible.

Also, doesn't Dijkstra also define the "do-nothing" procedure as "SKIP"?

Variable specification(?) and construction(?) and Hungarian notation
I think I understand the simplified explanation, but could you please provide a more complete one if you have the time and mood?

As opposed to Hungarian notation, I think it would make more sense to notate variables with both an abstract type and a type that refers to the underlying representation, at least in the specification as I know of no language that would support it. Possibly, we could define abstract types to be bounded to invariants. For example, "weekday" to be 0 to 7 (0 = undefined, 1 = Monday, ... and 7 = Sunday), and also "day" to be 0 to 31, with 31 being valid only in case "month == 1 or month == 3 ... or month == 12", 30 being valid only in case "month != 2", and 29 being valid only in case "month != 2 or (month == 2 and year % 4 == 0 and (year % 100 != 0 or year % 400 == 0))". Or maybe even the weekday could be constrained in a way so you can't say that 2020-10-09 is a Monday. In contrast to Hungarian notation, I think this could be checked more easily by an automated verification tool, though it would still be hard to do that for the entire state space.

Applications to well-known algorithms
I looked at the book for the maths, but I have trouble understanding this kind of maths. I know it's simply logic, but here we have specific constructs of a specific form. I think I need to do some exercises in predicate transformer semantics (Dijkstra's law as we have been calling it). Then, I should practice some algorithms by (re)specifying them in this notation.

State space transformations
I think I understand this one too, again of course in general. There have to be some more details though, but I can kind-of imagine them. I can also think of several analogous examples in both maths and computer science already.

Value actualization (initialization?) in a set
There is finally something I don't understand at all!

Could you please explain a little more about this one? How are the values of a set actualized? How are database operations and allocation strategies described?

In general it is the best practice to check inputs if they fulfill the prerequirements in every unit. But not always, for example with binary search (which requires a sorted array), you definitely don't want to check if the input array is sorted. There you make sure of it on the caller side that only sorted arrays are given as input.

It might be possible that formal verification tools could be able to check that at specification time. But they still need a lot more information about the inputs and outputs, and also about the data operated on in the meanwhile, than the software engineer or the programmer is usually willing to provide.

In short, I think that, in general, there are several related methodologies that have a similar terminology and similar goals, with only subtle differences. In any case, I think it makes sense to learn as many of them as possible, because one methodology might cover some aspects with more completeness and more clearness than another methodology, but also the opposite. Furthermore, even if you kind-of understand some aspect in one methodology, learning another methodology can help you further refine the understanding of this same aspect. That's my opinion, and I'm very pleased to have learned about Fóthism.

[bzt]

I'm however not sure whether I understand the phrase "You specify the problem instead that you want to solve", that is instead of what?

Instead of a formal state-space, you formally define a relation to describe what you want to achieve. The state-space is just defined informally as "every variable that's needed, but no more".

You got the concept of specification right. Instead of formally defining a relation on the state space (which is always accurate, but could be a huge task), from programming perspective it's easier to define preconditions and postconditions and some mathematical description of the algorithm. That's the point of specification.

This basically is modularity of procedures, I suppose?

Well, I would say modularity of everything (not just procedures, but procedures are part of it).

But I have a question. How do we notate conditionals that depend only on some parts of the state space (most common case in practice)? When we write an "if/else" statement, we don't put the entire state space inside the condition because that would be impractical or even impossible.

Yeah, I know my explanation wasn't good. If you take a look on an "if" program, then the state-space only contains variables which appear in it's condition (very simply put). So this is a vertical cut on the state-space of the entire program (in Hungarian it's called "altér", I guess sub-space maybe?). By the "conditional must cover the entire state-space" I mean horizontally, that is, all possible variable combinations are accounted for. For a typical "if" which has a boolean condition, that would be simple, true or false. However for a switch-like or if-else-chain conditional this makes a lot more sense. For example:

Code: Select all

if (a==1) {...} else
if (a==2) {...} else
if (b!=0) {...}

Here we must verify if this covers all the possibilities: is it true that "a" can have only two values (1 and 2) when "b" is zero? Do we left out some combinations of "a" and "b" incidentally? Is it okay if nothing happens in those cases? Etc. (So as you can see, this methodology won't solve your problems, but by defining rules on how to transcript your code into math it helps you discover potential mistakes. On the long run it teaches you how to develop best practices on your own,)

Also, doesn't Dijkstra also define the "do-nothing" procedure as "SKIP"?

Yeah, could be It was very long time ago that I've learned this.

As opposed to Hungarian notation, I think it would make more sense to notate variables with both an abstract type and a type that refers to the underlying representation, at least in the specification as I know of no language that would support it.

You are absolutely right about that, but not all languages support this, hence the need for Hungarian notation. (I mean Hungarian Apps.)

Possibly, we could define abstract types to be bounded to invariants. For example, "weekday" to be 0 to 7 (0 = undefined, 1 = Monday, ... and 7 = Sunday), and also "day" to be 0 to 31...

The Ada language for example supports this kind of invariants to some extent. This means it is easier to write a readable code in Ada. For example you can define a numeric type which can only hold the values 0 to 7. For more complex logic, like day can't have some values depending on month there's the generic abstraction. It is a bit stretch in this day/month example, but with generics you can describe an invariant regardless to the data representation type (so for example day and month can be stored on 8 bit or 64 bit or with float-point, the logic would remain the same).

I looked at the book for the maths, but I have trouble understanding this kind of maths. I know it's simply logic, but here we have specific constructs of a specific form.

Yeah, it can be frightening at first, I know. It has some unusual notations that you must get used to. Otherwise it is pretty simple actually.

Could you please explain a little more about this one? How are the values of a set actualized? How are database operations and allocation strategies described?

This is a bit complex topic, I agree. The idea is, you have an input set and a list of operations as input, and an updated set as an output. So instead of having a program that modifies a set, here you have another set describing the operations. For example, let's say you have A:= {a}, O:={(ins,b)} as input. After the O is interpreted, A can be either {a,b} or {b,a}, depending if your algorithm is FIFO or FILO (this is just a very simple example). Now checking correctness of this kinds of algorithms is pretty difficult, therefore this universal solution is defined with all the math. Now if you can track back your actual code to a variant of this universal one, then you only need to check the correctness of your transformations, which is easier. (And I must stress that this only cares about if your code is correct, performance is out of scope, that's for another semester.)

It might be possible that formal verification tools could be able to check that at specification time. But they still need a lot more information about the inputs and outputs, and also about the data operated on in the meanwhile, than the software engineer or the programmer is usually willing to provide.

Absolutely. But to prove correctness, the software engineer must provide it all, no workarounds, no shortcuts. I guess that's why it took years to prove correctness on the L4 kernel.

In short, I think that, in general, there are several related methodologies that have a similar terminology and similar goals, with only subtle differences.

Yes. There are differences, but the end of the day they must be similar since their goals are similar. No matter how many times people invent a hammer, it's always going to be look like a hammer

That's my opinion, and I'm very pleased to have learned about Fóthism.

You're welcome! I'm glad I could help!

Cheers,
bzt