PeterX wrote: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.
testjz wrote:I'd be interested to understand what are the main concepts of this methodology.
PeterX wrote: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