postcondition verification

Hello reader!

I have just made a program that takes a function or method signature with comments and generates a function that verifies postconditions of the function.
Download here(windows only so far). Click "Download 'cppAutoPostCon.exe' to your computer" at the bottom of the page.
Source here. Note that the only piece of code which is not inter platform is in the clipboard.cpp file. Feel free to port the code or use it for any purpose. Also note that with the source comes a project file for Code::Blocks IDE. Consult it if you want to build the code yourself because the set up is not trivial. Also note that the code has been compiled with GCC 4.4.1 and requires the Boost library v. 1.43.0 to be installed.

For example, it turns this:

//some text
//{{{ { a_setting_stuff ;;; a} {b} 
// {c_setting_stuff ;;; c} }}}
///some more text
ret_type do_sth(arg1,arg2,arg3)

into this:

bool verify_do_sth(ret_type _result,arg1,arg2,arg3)
{
    {
        a_setting_stuff;
        if(!(a))
            return false;
    }
    if(!(b))
        return false;
    {
        c_setting_stuff;
        if(!(c))
            return false;
    }
    return true;
}

Usage:
In your text editor select a function header with a comment.
Copy it to clipboard.
Run the program. (It will end in fraction of a second.)
The resulting verification function is now in the clipboard.
If the function could not be generated, the clipboard contains C++-style comment with an appropriate error message.

//edit 9th October
Now the program does much better job at formatting generated code, so that no line is too long to be legible and the indentation is acceptable.

Have fun verifying results of your function calls! (Yes, I know it sounds ridiculous. But the program is useful anyway.)

nlog(n)log(n) kd-tree construction using SAH

Disclaimer:
I don't know if anyone has ever invented this algorithm yet or not. A much more important fact is that I haven't found any intuitive explanation of it in the internet. Here is my attempt. Note that this article is inspired by a real piece of code, executing in my ray tracer.

Introduction

KD tree is a data structure, based on a space subdivision scheme. It is useful for fast search for shapes intersecting with a line in 3D space. Ray tracing is an obvious application of kd trees. The defining principle of a kd tree is that an axis-aligned bounding box of all shapes is split recursively into two child boxes, using an axis aligned plane. Each child box is going to have a list of all shapes that intersect with it. The split plane is positioned according to some kind of a sensible heuristic calculation. One of the best heuristics is the Surface Area Heuristic (SAH for short).
In this post I am not going to waste time repeating wildly accessible general information about kd trees and SAH. It is the fast use of geometry that is interesting in my method. Instead I would like to point the reader to materials that in my opinion explain it clearly enough:

http://en.wikipedia.org/wiki/Kd-tree
http://www.devmaster.net/articles/raytracing_series/part7.php (skip the beginning and go to 'kd trees' section)
http://www.devmaster.net/forums/showthread.php?t=15004

Now I assume that the reader knows how is kd-tree structured, what principles is SAH based on and what is the simple, naive algorithm for building the tree using SAH.

General outline of the method (also the naive method):

1. Find all position of the split planes which are worth consideration.
2. For each split position P:
2.1. Compute the coordinates that define the two boxes: one to the left and one to the right of the split plane.
2.2. Find the number NL of shapes that intersect left box and the NR of shapes that intersect the right box.
2.3. Calculate the SAH as NL*[the area of sides of the left box] + NR*[the area of sides of the right box]. There are usually some additional constants in this formula for adjusting the number of shapes per leaf, but they are not significant for the purpose of this post.
2.4. If the computed SAH value is the best so far, save it, together with the split position.
3. Take the best SAH value and check of it makes sense to split this node. If it is the case, compute the coordinates of the left and right box, create two children of this node and insert the intersecting shapes to them.

The most expensive step of the naive version is 2.2. In the naive version it involves checking if an intersection exists between each shape and the left/right box. This is O(n) step in an O(n) loop, which lifts the time complexity to O(n*n). It is done in each node of a tree, whose expected depth is O(log(n)), so the total expected complexity of the naive version of tree building is O(n*n*log(n)).

Lets assume, without the loss of generality, that the split axis is X (the split axis is the axis orthogonal to the splitting plane). My modification is based on observation that its not necessary to traverse all shapes for all possible split positions on X axis. Instead, I compute intersection (common part) of each shape with the node box and create two lists of all shapes, sorted by one of the extreme X positions of the intersection. First list is sorted by the minimal X values (later called 'Min'), second by the maximum X values (later called 'Max'). Note that for any split position P, all shapes which have Min <= P are going to intersect with the left child box (where 'left' is defined as having Xs smaller than P). Also, all shapes which have Max >= P are going to intersect the right box. The shape counts in the left and right box are simply the shape counts before and after certain elements on the Min and Max sorted lists. I can find those 'certain elements' in log(n) time if I use appropriate implementations of those lists.

Here is a more specific explanation of my modification.
I do additional precomputation in step 0:

0. For each shape compute the Min and Max coordinates of its intersection with box of the node. By intersection I mean common points of the shape and the box. For example an intersection of a box and a plane could be a rectangle. Only the coordinates on the axis orthogonal to the splitting plane are needed, so for each shape there will be just one pair of coordinates.
Create two sorted maps, containing all shapes:
  [Min]->[(shape pointer; an integer variable C, equal to 0)],
  [Max]->[(shape pointer; an integer variable C, equal to 0)].
Notation: In [a]->[b] a is a key, b is value and '->' means 'maps to'. (a;b) is a pair of elements a and b.
In fact, the maps above have to be multimaps, since min or max may be equal for multiple shapes. Any decent programming language should provide an abstraction of a sorted (multi)map, with logarithmic insertion and search operations. If your language provides a map, but does not provide multimap, you can use a map in which values are arrays of the pairs. If you use the C language, you can implement it as a balanced binary tree (e.g. red-black tree) or a skip list.
So far, the contents of the 0 step may be easily implemented by creating empty maps before the loop and inserting the shapes to them as soon as the min and max values are computed in each loop cycle. Then comes the assignment to the integer variables in the map:
  Initialize 'i' to 0.
  For each entry 'e' in the map:
    Set 'e'.value.C to 'i'.
    Increment 'i'.
This way each shape's map entry contains the number of shapes that preceed it in the map. Hence, the maps become:
  [Min]->[(pointer to S; count of shapes before S in this map)],
  [Max]->[(pointer to S; count of shapes before S in this map)].

Now the step 2.2 becomes:

2.2.Please, recall that we are interested in computing NL and NR, i.e. the counts of the shapes that intersect the left/right child box. Also recall that we are currently considering split position P.
Lets introduce integer Nt - the total shape count in the box (in other words: in both child boxes together). The calculation of NL an NR is as follows:
2.2.1 NL.
In the Min map find the first entry 'e' whose key is greater than P.
NL value will be equal to 'e'.value.C.
If there is no such entry (because P is greater than all Min keys), NL is equal to Nt.
2.2.2 NR.
In the Max map find first entry 'e', whose key is greater or equal to P.
NR value will be equal to Nt-('e'.value.C).
If there is no such entry (because P is greater than all Max keys), NR will be 0.

Any decent sorted map abstraction should provide a way of searching for the entries whose keys are most similar to given value, so I am not going to cover such search here. Note, however, that the complexity of 2.2.1 and 2.2.2 in a sorted map is log(n).

The rest of the algorithm stays the same. Actually, I think that this may also be implemented using a sorted array and binary search instead of the multimap, but I didn't want to obfuscate the explanation with too much generality, so I chose to refer to multimap concept consistently.

In the next post I am going to describe one more thing that may not be immediately obvious: how to compute the polygon created by intersecting a triangle with box. I am not going to cover shapes other than triangles since I solely use triangles, so I would not be writing from experience.

Boolmarks in Eclipse

This post is a credit of how shitty is the bookmarking functionality in Eclipse.
For the first, lets introduce the way bookmarking works there.
There are multiple ways of setting a bookmark:

Way 1: In the menu click Edit/Add Bookmark. Type something in the window that pops up. Click OK in it.
Way 2: Press ALT+E+K (a shortcut to the above). Type something in the window that pops up. Click OK in it.
Way 3: Right click on the strap to the left of where line numbers are present in the editor window (If you do not have line numbers, shame on you. In this case go to Window/Preferences/General/Editors/Text Editors and check "Show line numbers"). Choose Add bookmark from the drop down list. Type something in the window that pops up. Click OK in it.

Of course, as you might imagine, the whole reason why this functionality is shitty is the "Type something..." part in the above ways. This makes it completely unusable, since placing the bookmark is hardly worth the time and distraction spent on typing something and clicking OK in the pop-up. For example, when I'm coding, I want to bookmark 5 places where I need to make a modification, then jump to each, one by one, and make a modification.

It seems that the eclipse developers use bookmarks to jump to globally crucial places in whole projects. For those it may make sense to have names, since it is then easier to locate them from special place in the editor. The best reason for me to use bookmarks is to navigate in a single file.

For this reason I would like to introduce a naming convention: "global bookmarks" for the kind of thing implemented in Eclipse and "local bookmark" for the kind of thing I want to use (present e.g. in Code::Blocks, Borland and Visual Studio).
According to this naming convention, local bookmarks are missing from Eclipse. No more self-delusion, Eclipse developers!
This is something that definitely should be fixed. For the completeness of this post, I must mention that there is a bookmarks plugin at etc.to website, but its seems to be only for the Java version of Eclipse.

My rant on Eclipse+CDT

Eclipse is non-trivial to use for C++ and not designed for it. I am using Eclipse Galileo.
Problems:

CTD build system is a bit of a failure. It rebuilds project at wrong moments (e.g. sometimes after launching eclipse, even though the object files still exist. This makes it unusable for big projects. At some point I found out that this is caused by "use parallel builds" option, checked by default. This fact should be advertised as I am sure that it distracts many people.

In many cases CDT does not rebuild things properly which causes strange runtime errors. Somehow it assumes that programmer should know which sources to rebuild, which is a bad assumption because, if something can be automated, why not automate it? Things that confuse CDT seem to be more advanced language features, like complicated templates, together with static functions, global data, overloading, conditional compilation etc, in other words the further code is from pure C code, the more problems exist. Code::Blocks IDE always knows what to rebuild, probably because it uses make in less clever way.

Try do do "Project/Clean" without rebuilding. Guess what the eclipse shows in the console at the bottom?
Answer: "Build complete"
(The project is only cleaned, the message is confusing).

Right click an occurence of a function name. How do you go to definition?
Answer: You have to choose "Open Declaration".
Click the name in the definition and choose "Open Declaration" again. Where does it take you?
Answer: To the declaration.
Right click the declaration, choose "Open Declaration".
Answer: To the definition.

You are viewing a non-console window at the bottom, e.g. "Properties" or "Type Hierarchy". Click the launch button. What do you see at the bottom?
Still error log. The IDE should show the console since something is happening there.

When launching eclipse, the window which has the progress bar is behind applications that you already run (e.g. behind windows explorer).

Trying to launch debugger with errors in the code launches it.

After termination of an application, eclipse does not show the exit code. I have to switch to debug view to see it.

After pressing the "run" button Eclipse checks if there is anything to build, which often takes long time. I have lost many minutes of my life this way. It seems that there is no way of switching this off. It would be very convenient to just run the last built executable.

The first time you run the debugger you are asked about what kind of debugging you want. What the heck do the options mean?

When pressing SHIFT+CTRL+Right, editor selects part of the identifier, instead of the whole thing. When you double click using mouse pointer, it selects the whole thing, but there seems to be no way of doing it via keyboard. Perhaps this is good for Java, but its not for C++ where there are longer identifiers as well as different spelling conventions. Particularly, with the underscores between words, half of such partial selections are not what user wants, due to "landing" on the wrong side of the underscore. It seems sensible to have an option in editor to switch to selecting whole identifier.

When the "Project Explorer" tab looses focus (this happens frequently), Eclipse somehow does not know which is the active project, so, for example, the "build" and "launch" buttons don't know which project to build or launch. This is silly since I believe most people work on single project most of the time. This also causes possible slip mistakes when user selects things in the dialog boxes that appear when he presses the buttons.

After excluding a file from build (right click on file in Project Explorer and choosing "Exclude from Build", it is not clear how to bring it back, because there is no symmetric "Include to Build" option. An unaware programmer may get stuck in the middle of a task (as I did). The option is available after the same right click, in "Properties" menu in "C/C++ Build" section.

BTW, I am using Eclipse anyway due to rich semantic help, rich set of keyboard shortcuts, syntax analysis which points out syntax errors immediately and showing compile errors in many places in IDE.

sprytniejsze budowanie zbiorcze

Jest sobie duży projekt w C++? Jest problem z czasem kompilacji z powodu dużej liczby jednostek translacji(plików cpp)? Oto proste rozwiązanie, oparte na znanej idei budowania zbiorczego, czyli "unity build" (zwanej też "uber build" albo "bulk build"), polegającej na #includowaniu plików cpp do zbiorczego pliku cpp i kompilowaniu jego zamiast rzeczonych plików.

Cechą unikatową rozwiązania, które zaraz opiszę jest to, że:
A) Nie trzeba męczyć się z ręcznym wybieraniem plików, które mają być skompilowane. Po prostu kompilujemy wszystkie pliki cpp (w przeciwieństwie do powyżej realizacji "unity build").
B) Można dowolnie przełączać pomiędzy "unity build" a normalną kompilacją.

Cały mechanizm zadziała automatycznie, jedyną rzeczą, która sygnalizuje chęć skorzystania z unity build jest dodanie jednej opcji polecenia wywołującego linker.

Aby zaimplementować mechanizm, wystarczy zrobić 2 rzeczy:
A) W każdym pliku cpp dopisać na początku (przed poleceniami #include)
#if defined(IN_COLLECTIVE) or not defined(BUILD_COLLECTIVELY)
a na końcu
#endif
B) W każdym folderze zrobić plik zbiorczy collective.cpp, wyglądający mniej więcej tak:
#ifdef BUILD_COLLECTIVELY
#define IN_COLLECTIVE
#include"A.cpp"
#include"B.cpp"
#include"C.cpp"
#include"D.cpp"
#include"E.cpp"
#undef IN_COLLECTIVE
#endif

Oczywiście A,B,C,D,E to nazwy plików cpp w folderze, gdzie znajduje się plik z powyższym kodem.

W efekcie, jeśli dodamy do opcji linkera makrodefinicję BUILD_COLLECTIVELY, to program zbuduje nam się kilka razy szybciej. Jeżeli nie, to wszystko będzie po staremu. Podkreślam, że BUILD_COLLECTIVELY możemy dodać do wywołania linkera, np.
g++ -DBUILD_COLLECTIVELY ..., nie musimy w żadnym pliku nagłówkowym.
Nie będę tu gęsto tłumaczył dlaczego to przyspiesza kompilację, ani nie będę wymieniał wszystkich zalet i wad "unity build", najlepiej odeślę do materiałów poglądowych:
http://buffered.io/2007/12/10/the-magic-of-unity-builds/
http://stackoverflow.com/questions/861707/is-reducing-number-of-cpp-translation-units-a-good-idea
a tutaj tylko zakreślę przyczynę: chodzi głównie o to, że wszystkie includowane nagłówki są przetwarzane tylko raz, a nie tyle razy, ile jest plików cpp.

W pierwszym linku powyżej są opisywane rozwiązania polegające na wyłączeniu z kompilacji wszystkich plików cpp poza zbiorczym lub też tworzeniu osobnego projektu do budowania zbiorczego. Moje rozwiązanie stanowi ulepszenie w stosunku do nich, dlatego, że w praktyce jeżeli pliki są wyłączane z projektu w ulubionym IDE lub kod jest wyłączony kompilacją warunkową, ciężko jest zmusić IDE do włączenia w takim kodzie pomocy kontekstowej, podświetlania znaczeniowego i innych udogodnień. W moim rozwiązaniu do wygodnej pracy nad tym kodem wystarczy nie zdefiniować BUILD_COLLECTIVELY (czyli tak naprawdę nie trzeba robić nic).

Zauważ, że rozwiązanie jest całkowicie transparentne, tzn jeżeli kolega zacznie pracować nad naszym kodem i utworzy sobie do tego celu nowy projekt, to domyślnie będzie miał stary, znany mu sposób budowania, pomoc kontekstową i nie będzie musiał nic dodatkowo ustawiać, żeby w ogóle zacząć pracę.

Zauważ również, że w wymienionych wymienionych powyżej krokach nie ma nic, czego nie mógłby dopisać prosty skrypt, można więc z łatwością zaimplementować to rozwiązanie w naprawdę dużym projekcie.

_________

________

PS.
Nawiasem mówiąc, ten demotywator dwa wpisy wcześniej "Eigenfaces..." mógłby chyba wygrać konkurs na najbardziej niszowy demotywator w historii (proszę, wyprowadźcie mnie z błędu, pokażcie jeszcze lepszy!). Nie dość, że dotyczy bardzo wąskiej dziedziny (uczenie się maszyn), to jeszcze zakłada posiadanie zawoalowanej wiedzy praktycznej z zakresu maszynowego rozpoznawania twarzy, a do tego jest tak pięknie niejednoznaczny, że jednocześnie chyba wymaga rozumienia poezji. Dla niekumatych dodam, że "eigenfaces" to takie pomocnicze reprezentacje twarzy, pomagające np. w określaniu, czy twarz ze zdjęcia to twarz konkretnej osoby (w dużym uproszczeniu). W demotywatorze chodzi o to, że student spał i śniły mu się, jak mu się wydawało, diabelnie nieprawdopodobne rzeczy, godne mar sennych, ale, jak się okazuje, te rzeczy są jak najbardziej rzeczywiste, w zasięgu dzisiejszej nauki. Te nieprawdopodobne rzeczy, to automatyczne wykrywanie twarzy śpiących studentów wśród innych, nieśpiących, używając przykładowych zdjęć i określenia, czy przykłady przedstawiają śpiących, czy nie. Twarz tego diabełka, to tytułowy eigenface, z dodatkiem różków i kłów. Diabelność ma podkreślać nierzeczywistość. Słowa "sleeping student" mają już ostatecznie zwrócić uwagę na sen, co ma ułatwić wpadnięcie na to, że student na w drugiej części właśnie się obudził. Aha, tak dla wyjaśnienia, pomyślałem, że komentarz do wpisu nie zasługuje na osobny wpis, więc piszę to w "PS".

Reklama na tvn24.pl

Dzieciom życzymy kochających nowych właścicieli.

Refleksje na temat inteligentnych wskaźników w C++ i projektowania programu.

Czy je polecam?
Tylko początkującym.
Czy coś dają?
I tak i nie.

Czemu "tak"?

Chciałbym zwrócić uwagę czytelnika na zaletę tych wskaźników,
nie będącą kolejnym powtarzaniem, że umożliwiają niepisanie 'delete'.

W przeciwieństwie do referencji z Javy czy C# inteligentne wskaźniki nadal wymuszają dobry projekt programu, robiąc problemy ze względu na cykle referencji. Konkretnie, w przypadku cyklu A-B-A wymuszają, żeby np. obiekt A miał inteligentny wskaźnik do B a B tylko zwykły wskaźnik do A. To jawnie wskazuje, który obiekt jest właścicielem
drugiego. To nie daje tylko destrukcji we właściwej kolejności. To również wymusza strukturę właścicielską.

Nazwijmy słowem "właściciel" jakiś obiekt, który ma inteligentny wskaźnik na inny obiekt. Program zbudowany w ten sposób jest acyklicznym grafem skierowanym (DAGiem) z właścicielem wszystkiego jako korzeń. Nad takim kodem dużo łatwiej jest zapanować niż nad dowolnym grafem, gdzie użycie jakiegoś konkretnego elementu jest bardzo utrudnione bo nigdy nie wiadomo, jakie obiekty trzeba mu dać, gdzie go stworzyć, w jakiej kolejności wykonać inicjalizację itd. W dagu, jak jest właściciel, to
można go poprosić o stworzenie jakiejś posiadłości. To właśnie właściciel albo od razu potrafi stworzyć posiadłość, bo miał wymuszoną inicjalizację, albo ma dobrą dokumentację i jakieś asercje uniemożliwiające tworzenie rzeczy w niewłaściwej kolejności.

Dag wykazuje duże podobieństwo do drzewa, zatem łatwo go, albo jakiś jego sektor w drzewo zamienić, czyniąc projekt jeszcze bardziej eleganckim. Przeprojektowanie dagu też jest prostsze, niż zwykłego grafu, bo zmiany będą miały wpływ tylko na określony podgraf, nie na cały system. W przypadku zaś, gdy robimy program współbieżny, daje to możliwość uruchomienia współbieżnie podgrafów tam, gdzie się rozłączają, bez obaw że gdzieś poza wspólnym właścicielem są jakieś współdzielone dane, które wymagają synchronizacji.

Kwestia poprawnego zaprojektowania programu mogłaby być przez kogoś zrozumiana jako zrobienie takiego programu, gdzie poprawnie działają tworzenie i niszczenie obiektów i dzięki temu nie ma np.odniesienia przez wskaźnik z adresem null lub przedwczesnego niszczenia obiektu. Problem w tym, że niektóre tego typu błędy wynikają ze złego projektu a niektóre to po prostu zwykłe usterki techniczne, spowodowane np. nienapisaniem 'delete'. Inteligentne wskaźniki, eliminując niektóre proste błędy pozwalają oddzielić te dwa zagadnienia. Jako efekt uboczny, możliwe jest łatwiejsze eksperymentowanie ze strukturą programu, bez obaw że gdzieś zapomni się 'delete'.

Czemu "nie"?

Jeśli potrafi się dobrze projektować program jako dag, to nie dadzą dużo, bo kolejność destrukcji jest jak najbardziej spójna i problem sprowadza się do napisania 'delete' dla każdego 'new', a to można osiągnąć zwykłym opakowaniem, nie wspierającym inteligentnego współdzielenia obiektu.

Inteligentne wskaźniki zabierają jednak trochę czasu, bo są z nimi czasami duże problemy. Problemem może być np. to, że jakiś obiekt jest przedwcześnie niszczony, gdy inteligentny wskaźnik przez przypadek na moment zamienia się na zwykły po to, by zaraz znowu przemienić się w inteligentny. Wtedy obiekt jest niepotrzebnie niszczony i ciężko jest potem znaleźć taki błąd, często objawiający się gdzieś daleko od zręcznie zakamuflowanego przez niejawne wywołanie destruktora miejsca zniszczenia. Gdzieś spotkałem się nawet z określeniem "smark pointers", nawiązującym do tego problemu.

Innym problemem są częste problemy z debugowaniem niszczenia obiektów, które są niszczone przez destruktory obiektów globalnych. Brak jawności destrukcji sprawia wtedy więcej szkody niż pożytku, bo pisząc ją jawnie mamy przynajmniej pewność, że jeżeli wszystko zadziała, to zadziała w określony przez nas sposób.

Jest jeszcze inny problem. Konkretnie to może się zdarzyć, że inteligentny wskaźnik na dany obiekt może zostać stworzony więcej niż raz, nie kopiowaniem wskaźnika, tylko z surowego adresu. To również powoduje przedwczesne zniszczenie obiektu. Jest strategia zapobieżenia temu, konkretnie stworzenie globalnej mapy (adres->licznik odniesień), gdzie wskaźniki sprawdzałyby liczbę odniesień, zamiast przechowywać ją bezpośrednio samemu. To jednak wymaga danych globalnych i przez to sprawia olbrzymie problemy we współbieżnym kodzie.


Werdykt

Ostatecznie mój werdykt jest następujący: nie używać inteligentnych wskaźników, które utrudniają życie i nie przerzucać się na Javę, gdzie wszyscy współpracownicy będą uprawiać w projekcie wolną Amerykankę, rzygając w czasach kryzysu obiektami NullPointerException. Projektować dobrze program i używać w klasie-właścicielu opakowania (np. auto_ptr) na posiadany obiekt.

EDIT: (Żeby nie wywoływać świętej wojny Java kontra C++, dodam, że mam zastrzeżenia do zbyt luźnego modelu orientowania obiektowego w Javie, natomiast nie mam ich samej Javy jako platformy, bo ilość bibliotek standardowych sprawia, że każdy powinien przynajmniej rozważyć Javę jako język do swojego nowego projektu).