Tudd Intuíció, előadás, épít ciklus segítségével invariáns
Kivonat: Az építőiparban a ciklus program „eddig” segítségével az invariáns, azaz jóváhagyás, amely a tárolt egyes A ciklus végrehajtása szervezetben. Alkalmazás e rendszer lehetővé teszi, hogy tudatosan építeni egy olyan algoritmus, és bizonyítani a helyességét a munkáját a szöveget, anélkül, hogy a tesztelés. Alkalmazása áramkör a példákban szemléltetjük: euklideszi algoritmus, a legnagyobb közös osztó algoritmus gyors hatványozás kiterjesztett euklideszi algoritmus, a közelítő számítást a logaritmus használata nélkül a sorozat bővítése.
Megfelelő használatát a tervezési ciklusban mindig némi nehézséget. A használata elemi elmélete segít elkerülni a hibákat, és megkönnyíti az írás komplex programok.
Az alapötlet a következő. beállított értékek változók változik végrehajtása során a hurok. Meg kell találni a kapcsolatát a változó változók állandó marad. Ez az arány az úgynevezett invariáns ciklust. Tudatos építési ciklus „míg a” mindig jár az explicit megfogalmazása és használata hurok invariáns.
Explicit invariáns készítmény segít, hogy írjon az inicializálás változók előtt végzett a ciklus kezdetén. és a test a hurok. Inicializálás biztosítania kell, hogy az invariáns kezdete előtt a ciklust. A hurok testet úgy kell kialakítani, hogy az biztosítsa a megőrzése az invariáns. (Pontosabban az a tény, hogy az invariáns előtt végzünk a végrehajtás a ciklus törzse. Változtatható végrehajtását kell követnie miután a szervezet bezárását ciklust. Végrehajtása során a hurok test lehet törött állandó).
Alkatrészek a ciklust. általában együtt járó csökkent mértékű. amely monoton növekszik vagy csökken monoton minden A ciklus végrehajtása szervezetben. Cycle „eddig” befejeződött, amikor a feltétele után a „most” a fejlécben ciklus hamissá válik. Ezért ez a feltétel függ közvetlenül vagy közvetve az érték egy monoton csökkenő vagy növekvő végrehajtása során ciklusban. A cél elérése érdekében a fajlagos érték feltétel kell válnia hamis. A feltétel az úgynevezett ciklus befejeződött tagadása feltételeinek folyamatos után a „amíg” a címe a ciklus.
A hurok invariáns, míg megszűnése feltételeket kell megoldást nyújtanak a kívánt feladatot.
általános sematikus
Legyen X halmaza minden lehetséges értékeinek halmazai az összes változót, hogy a változás során a ciklus. A beállított X néha egy fázis, vagy kialakítást, a tér problémát. Változtatható - ez a feltétele a I (x). függ a pont a több X x és figyelembe értékek „true” vagy „false”. (Matematikusok nevezik az ilyen feltétel predikátumok.) Az inicializálás során pont x kap értéket x0. ezt a feltételt I (x0) igaz.
Jelöljük a hurok állapot befejezése után a Q (x). Feltétel I (x) és Q (x) úgy kell megválasztani, hogy egyidejűleg az igazság az I (x) és Q (x) megoldást nyújt a kívánt célok: megtalálni azt a pontot x a kívánt tulajdonságokkal.
A hurok test lehet értelmezni, mint egy leképezés pont egy új pont x T (x) az azonos több X:
Feltételek I (X) invariáns megjelenítéséhez T. Ha I (x) igaz, akkor én (T (x)) is igaz.
Általános építési ciklus diagramban invariáns az alábbiak szerint:
Természetesen ez a rendszer nem érték nélkül képes alkalmazni a gyakorlatban. Tekintsük néhány fontos példát annak használatát.