Zadacha verifikacii programmnogo obespecheniya stanovitsya segodnya vse bolee vostrebovannoj, tak kak slozhnost' programmnyh sistem s kazhdym dnem postoyanno rastet, i my vse bol'she stalkivaemsya s temi ili inymi sboyami v ih rabote. Invariantom v programmirovanii nazyvaetsya logicheskoe vyrazhenie, zavisyashhee ot peremennyh v tele cikla i istinnoe, kak pered ego vypolneniem, tak i posle. Znanie invarianta dlya konkretnogo cikla pozvolyaet vypolnit' proverku na korrektnost' ego raboty. V dannoj knige delaetsya popytka razrabotki takoj programmnoj sistemy, kotoraya pozvolila by realizovat' avtomaticheskij poisk invariantov dlya konkretno zadannyh ciklov i chastichno avtomatizirovat' process verifikacii programm. Dannaya kniga budet interesna i polezna, kak opytnym programmistam, tak i tem, kto prosto interesuetsya problemoj verifikacii programmnogo obespecheniya.