Adott egy függvénykompozíció, amelynek értékét a sorozatban adott argumentumokra kell elemenként meghatározni. Tegyük fel, hogy , az adatok száma nagysegrendekkel nagyobb a függvénykompozícióban szereplő függvénykomponensek számánál. Feltételezzük azt is, hogy az egyes függvénykomponensek kiszámításához szükséges idő lényegében azonos. Ha elegendő processzor áll rendelkezésre, akkor megszervezhetjük az eredmény kiszámítását oly módon, hogy az egyes komponesfüggvények kiszámítását egy-egy processzorra bízzuk. Először kiszámítjuk értékét az első adatra -re. Ennek eredményét -et továbbadjuk a következő processzornak, amelyik kiszámítja -et. Közben az első processzor megkapja a második adatot, -t és meghatározza -t. lépés után feltöltődik az adatcsatorna, az első adat eljut a . függvénykomponenst számoló processzorig, majd minden további lépésben egy-egy újabb adatra kapunk végeredményt. Ha a kommunikációs költségeket figyelmen kívül hagyjuk, akkor arra a következtetésre jutjatunk, hogy processzorral az adatból álló sorozatra lépésben elő tudjuk állítani a végeredményt, míg ugyanezt egyetlen processzoron lépésben tudnánk megtenni. Tekintettel arra, hogy , ezért a két lépésszám hányadosa: , azaz processzorral kb. -szer gyorsabban végzünk.

A formális specifikáció során először csak annyit fogalmazunk meg, hogy egy összetett függvény értékét kell elemenként meghatározni a sorozatra. A sorozat elemei az csatornán vannak kezdetben, újabb adat nem érkezik a későbbiekben és fixpontban az eredmény, az sorozat az sorozat történetében található meg. Ez azt jelenti, hogy az eredmények rendre rákerültek az csatornára, de esetleg már nincsenek ott.

A . kikötés szerint az és története kezdetben tartalmazza a sorozatot, és a 26.84. kikötés szerint az sorozat tötrénete nem is változhat, tehát újabb elem nem kerülhet az csatornára. refpipe1. szerint az csatorna kezdetben üres. Fixpontban . szerint megköveteljük, hogy az története éppen legyen. A . kikötés szerint a programnak terminálnia kell.

A megoldás előállításához bővítjük az állapotteret az csatornaváltozókkal és történetváltozóikkal a . ábrának megfelelően és finomítjuk a specifikációt a fixpontfinomítás tétele alapján (, ), illetve variánsfüggvényt vezetünk be ().

A . pontban bevezetett variáns függvény értékét úgy határozzuk meg, hogy a rendezett n-es elemeit helyiértékkel súlyozzuk, az egyes csatornákon lévő elemek száma rendre egy alapú számrendszerben felírt szám számjegyeinek felel meg.

A fixpontfinomítás tétele alapján belátjuk, hogy az új specifikáció finomítása az eredetinek. Megmutatjuk, hogy: .

Jelölje az első függvény kompozícióját: . Teljes indukcióval belátható, hogy . A lemmából -re következik az állítás.

Az alábbi program megfelel a finomított specifikációnak.

26.14. ábra -

26.12. ábra. Adatcsatorna