Zadacha verifikatsii programmnogo obespecheniya stanovitsya segodnya vse bolee vostrebovannoy, tak kak slozhnost' programmnykh sistem s kazhdym dnem postoyanno rastet, i my vse bol'she stalkivaemsya s temi ili inymi sboyami v ikh rabote. Invariantom v programmirovanii nazyvaetsya logicheskoe vyrazhenie, zavisyashchee ot peremennykh v tele tsikla i istinnoe, kak pered ego vypolneniem, tak i posle. Znanie invarianta dlya konkretnogo tsikla pozvolyaet vypolnit' proverku na korrektnost' ego raboty. V dannoy knige delaetsya popytka razrabotki takoy programmnoy sistemy, kotoraya pozvolila by realizovat' avtomaticheskiy poisk invariantov dlya konkretno zadannykh tsiklov i chastichno avtomatizirovat' protsess verifikatsii programm. Dannaya kniga budet interesna i polezna, kak opytnym programmistam, tak i tem, kto prosto interesuetsya problemoy verifikatsii programmnogo obespecheniya.