Da bismo razmatrali ispravnost programa uvodimo pojam Horove
trojke:
{φ} P {ψ}
sa sledećim značenjem: ako tvrđenje φ važi neposredno pre izvršavanja programa P tada
će nakon izvršavanja programa P važiti tvrđenje ψ.
Tvrđenje φ naziva se preduslov, a tvrđenje ψ pauslov (posleuslov ili postuslov) i zajedno čine specifikaciju programa P. Ova tvrđenja se iskazuju u logici prvog reda.
Prethodna definicija je neprecizna, jer nije jasna za slučaj da izvršavanje programa P ne staje. Zbog toga razlikujemo:
Ukoliko se ne naglasi drugačije, koristićemo pojam Horove trojke u smislu parcijalne korektnosti.
Primeri Horovih trojki:
Primer 1. {X=1} X=X+1; {X=2}
U ovom primeru preduslov je da je X jednako 1, a pauslov da je X jednako 2. Program se sastoji od naredbe dodele, vrednost promenljive X postaje X+1. Ako se naredba dodele izvršava nakon što je ispunjen preduslov i ako se to izvršavanje zaustavi (što u ovom slučaju sigurno važi), jasno je da će biti ispunjen i pauslov. U ovom primeru, program zadovoljava datu specifikaciju.
Primer 2. {X=1} Y=X; {Y=1}
U ovom primeru preduslov je da je X jednako 1, a pauslov da je Y jednako 1. Program se sastoji od naredbe dodele, vrednost promenljive Y postaje X. Ako se naredba dodele izvršava nakon što je ispunjen preduslov i ako se izvršavanje naredbe dodele završi, tada će nakon izvršenja naredbe biti ispunjen i pauslov. I u ovom primeru specifikacija je tačna.
Primer 3. {X=1} Y=X; {Y=2}
U ovom primeru preduslov je da je X jednako 1, a pauslov da je Y jednako 2. Program se sastoji od naredbe dodele, vrednost promenljive Y postaje X. Ako se naredba dodele izvršava nakon što je ispunjen preduslov i ako se to izvršavanje zaustavi, tada nakon izvršenja naredbe neće biti ispunjen pauslov. U ovom slučaju specifikacija nije tačna.
Primer 4. {X=x & Y=y} BEGIN R=X; X=Y; Y=R; END {X=y & Y=x}
Značenje ove Horove trojke je da ako se naredbe programa BEGIN R=X; X=Y; Y=R; END izvrše, tada će promenljive X i Y razmeniti svoje vrednosti, što je tačno.
Primer 5. {X=x & Y=y} BEGIN X=Y; Y=X; END {X=y & Y=x}
Značenje ove Horove trojke je da ako se naredbe programa BEGIN X=Y; Y=X; END izvrše tada će promenljive X i Y razmeniti svoje vrednosti. Ovo, naravno, nije tačno.
Primer 6. {true} P {ψ}
Značenje ove Horove trojke je da kad god se izvršavanje programa P zaustavi, važi uslov ψ .
Primer 7. {φ} P {true}
Ova specifikacija je tačna za sve preduslove φ i sve programe P, jer je true uvek tačno.