Twierdzenie o programie strukturalnym - Structured program theorem

Graficzna reprezentacja trzech podstawowych wzorców twierdzenia o programie strukturalnym — sekwencja, selekcja i powtórzenie — za pomocą diagramów NS (niebieski) i schematów blokowych (zielony).

Strukturze twierdzenie Program , zwany również twierdzenie Böhm-Jacopini , to wynik w programowaniu teorii języka . Stwierdza, że ​​klasa grafów przepływu sterowania (historycznie nazywana w tym kontekście schematami blokowymi ) może obliczyć dowolną obliczalną funkcję, jeśli łączy podprogramy tylko na trzy określone sposoby ( struktury kontrolne ). To są

  1. Wykonanie jednego podprogramu, a następnie innego podprogramu (sekwencji)
  2. Wykonanie jednego z dwóch podprogramów zgodnie z wartością wyrażenia logicznego (wybór)
  3. Wielokrotne wykonywanie podprogramu, o ile wyrażenie logiczne jest prawdziwe (iteracja)

Wykres strukturalny podlegający tym ograniczeniom może jednak wykorzystywać dodatkowe zmienne w postaci bitów (przechowywane w dodatkowej zmiennej całkowitej w oryginalnym dowodzie) w celu śledzenia informacji, które oryginalny program reprezentuje przez lokalizację programu. Konstrukcja została oparta na języku programowania Böhma P′′ .

Twierdzenie to stanowi podstawę programowania strukturalnego , paradygmatu programowania, który unika poleceń goto i używa wyłącznie podprogramów, sekwencji, selekcji i iteracji.

Pochodzenie i warianty

Twierdzenie to jest zwykle przypisywane do artykułu Corrado Böhma i Giuseppe Jacopiniego z 1966 roku . David Harel napisał w 1980 roku, że artykuł Böhma-Jacopiniego cieszył się „powszechną popularnością”, szczególnie wśród zwolenników programowania strukturalnego. Harel zauważył również, że „ze względu na dość techniczny styl [artykuł Böhm-Jacopiniego z 1966 r.] jest najwyraźniej częściej cytowany niż czytany szczegółowo” i po przejrzeniu dużej liczby artykułów opublikowanych do 1980 r. Harel argumentował, że treść Dowód Böhma-Jacopiniego był zwykle błędnie przedstawiany jako twierdzenie ludowe, które zasadniczo zawiera prostszy wynik, który sam w sobie można prześledzić od powstania nowoczesnej teorii obliczeniowej w pracach von Neumanna i Kleene'a .

Harel pisze również, że bardziej ogólna nazwa została zaproponowana przez HD Millsa jako „The Structure Theorem” na początku lat siedemdziesiątych.

Pojedyncza pętla, ludowa wersja twierdzenia

Ta wersja twierdzenia zastępuje cały przepływ sterowania oryginalnego programu pojedynczą whilepętlą globalną , która symuluje licznik programu przechodzący przez wszystkie możliwe etykiety (pola schematu blokowego) w oryginalnym programie bez struktury. Harel prześledził pochodzenie tego ludowego twierdzenia w dwóch pracach oznaczających początek informatyki. Jednym z nich jest opis architektury von Neumanna z 1946 r. , który wyjaśnia, w jaki sposób licznik programu działa w odniesieniu do pętli while. Harel zauważa, że ​​pojedyncza pętla używana przez ludową wersję twierdzenia o programowaniu strukturalnym w zasadzie zapewnia semantykę operacyjną do wykonania schematu blokowego na komputerze von Neumanna. Innym, jeszcze starszym źródłem, w którym Harel wyśledził ludową wersję tego twierdzenia, jest twierdzenie Stephena Kleene o postaci normalnej z 1936 roku.

Donald Knuth skrytykował tę formę dowodu, która prowadzi do pseudokodu takiego jak ten poniżej, wskazując, że struktura oryginalnego programu jest całkowicie tracona w tej transformacji. Podobnie Bruce Ian Mills napisał o tym podejściu, że „Duch struktury blokowej jest stylem, a nie językiem. Symulując maszynę Von Neumanna, możemy wytworzyć zachowanie dowolnego kodu spaghetti w ramach języka o strukturze blokowej. To nie oznacza, że ​​nie jest to spaghetti.”

p := 1
while p > 0 do
    if p = 1 then
        perform step 1 from the flowchart
        p := resulting successor step number of step 1 from the flowchart (0 if no successor)
    end if
    if p = 2 then
        perform step 2 from the flowchart
        p := resulting successor step number of step 2 from the flowchart (0 if no successor)
    end if
    ...
    if p = n then
        perform step n from the flowchart
        p := resulting successor step number of step n from the flowchart (0 if no successor)
    end if
end while

Dowód Böhma i Jacopiniego

Dowód w pracy Böhma i Jacopiniego przebiega przez indukcję na strukturze schematu blokowego . Ponieważ wykorzystywał dopasowywanie wzorców w grafach , dowód Böhma i Jacopiniego nie był tak naprawdę praktyczny jako algorytm transformacji programu , a tym samym otworzył drzwi do dodatkowych badań w tym kierunku.

Implikacje i udoskonalenia

Dowód Böhma-Jacopiniego nie rozstrzygnął kwestii, czy przyjąć programowanie strukturalne do tworzenia oprogramowania, częściowo dlatego, że konstrukcja częściej zaciemniała program niż go ulepszała. Wręcz przeciwnie, sygnalizował początek debaty. Słynny list Edsgera DijkstryIdź do oświadczenia uważanego za szkodliwy ” został wydany w 1968 roku.

Niektórzy naukowcy przyjęli purystyczne podejście do wyniku Böhma-Jacopiniego i argumentowali, że nawet instrukcje takie jak breaki returnze środka pętli są złą praktyką, ponieważ nie są potrzebne w dowodzie Böhma-Jacopiniego, i dlatego zalecali, aby wszystkie pętle miały jedną punkt wyjścia. To purystyczne podejście jest urzeczywistnione w języku programowania Pascal (opracowanym w latach 1968-1969), który do połowy lat 90. był preferowanym narzędziem do prowadzenia zajęć wprowadzających z programowania w środowisku akademickim.

Edward Yourdon zauważa, że ​​w latach 70. istniał nawet filozoficzny sprzeciw wobec przekształcania programów nieustrukturyzowanych w ustrukturyzowane za pomocą zautomatyzowanych środków, w oparciu o argument, że trzeba od samego początku myśleć w sposób programowania ustrukturyzowanego. Pragmatycznym kontrapunktem było to, że takie przekształcenia przyniosły korzyści dużej części istniejących programów. Wśród pierwszych propozycji zautomatyzowanej transformacji była praca Edwarda Ashcrofta i Zohara Manny z 1971 roku .

Bezpośrednie zastosowanie twierdzenia Böhma-Jacopiniego może skutkować wprowadzeniem dodatkowych zmiennych lokalnych do wykresu strukturalnego, a także może spowodować pewne powielenie kodu . Ta ostatnia kwestia nazywa się w tym kontekście problemem półtora pętli . Oba te problemy dotyczą Pascala i według badań empirycznych cytowanych przez Erica S. Robertsa studenci programiści mieli trudności z formułowaniem poprawnych rozwiązań w Pascalu dla kilku prostych problemów, w tym napisania funkcji do wyszukiwania elementu w tablicy. Badanie przeprowadzone przez Henry'ego Shapiro z 1980 r., cytowane przez Robertsa, wykazało, że używając wyłącznie struktur kontrolnych dostarczonych przez Pascala, poprawne rozwiązanie podało tylko 20% badanych, podczas gdy żaden z badanych nie napisał niepoprawnego kodu dla tego problemu, jeśli pozwolono mu na napisanie odpowiedzi z środek pętli.

W 1973 r. S. Rao Kosaraju udowodnił, że można uniknąć dodawania dodatkowych zmiennych w programowaniu strukturalnym, o ile dozwolone są arbitralnie głębokie, wielopoziomowe przerwy w pętlach. Co więcej, Kosaraju udowodniło, że istnieje ścisła hierarchia programów, obecnie nazywana hierarchią Kosaraju , w której dla każdej liczby całkowitej n istnieje program zawierający wielopoziomowe przerwanie głębokości n , którego nie można przepisać jako program z wielopoziomowymi przerwami głębokość mniejsza niż n (bez wprowadzania dodatkowych zmiennych). Kosaraju przywołuje wielopoziomową konstrukcję łamania do języka programowania BLISS . Wielopoziomowe przerwy, w postaci słowa kluczowego, zostały wprowadzone w wersji BLISS-11 tego języka; oryginalny BLISS miał tylko jednopoziomowe przerwy. Rodzina języków BLISS nie zapewniała nieograniczonego goto. Język programowania Java będzie później również podążał za tym podejściem. leave label

Prostszym wnioskiem z artykułu Kosaraju jest to, że program można zredukować do programu strukturalnego (bez dodawania zmiennych) wtedy i tylko wtedy, gdy nie zawiera pętli z dwoma różnymi wyjściami. Redukowalność została zdefiniowana przez Kosaraju, mówiąc luźno, jako obliczanie tej samej funkcji i używanie tych samych „prymitywnych działań” i predykatów, co oryginalny program, ale prawdopodobnie przy użyciu różnych struktur przepływu sterowania. (Jest to węższe pojęcie redukowalności niż to, którego używał Böhm-Jacopini.) Zainspirowany tym wynikiem, w sekcji VI swojego wysoko cytowanego artykułu, który wprowadził pojęcie złożoności cyklomatycznej , Thomas J. McCabe opisał analogię twierdzenia Kuratowskiego dla grafy przepływu sterowania (CFG) programów nieustrukturyzowanych, to znaczy minimalne podgrafy, które sprawiają, że CFG programu nie ma struktury. Te podgrafy mają bardzo dobry opis w języku naturalnym. Oni są:

  1. rozgałęzienie pętli (inne niż z testu cyklu pętli)
  2. rozgałęzianie się w pętlę
  3. rozgałęzianie się na decyzję (tj. na „oddział”)
  4. odgałęzienie od decyzji

McCabe faktycznie odkrył, że te cztery grafy nie są niezależne, gdy pojawiają się jako podgrafy, co oznacza, że ​​koniecznym i wystarczającym warunkiem, aby program nie miał struktury, jest to, aby CFG miał jako podgraf jeden z dowolnego podzbioru trzech z tych czterech grafów. Odkrył również, że jeśli program nieustrukturyzowany zawiera jeden z tych czterech podgrafów, to musi zawierać inny odrębny ze zbioru czterech. Ten ostatni wynik pomaga wyjaśnić, w jaki sposób przepływ sterowania nieustrukturyzowanego programu zostaje uwikłany w to, co jest popularnie nazywane „ kodem spaghetti ”. McCabe wymyślił również miarę liczbową, która, biorąc pod uwagę dowolny program, określa ilościowo, jak daleko jest od ideału bycia programem ustrukturyzowanym; McCabe nazwał swoją miarę podstawową złożonością .

Charakterystykę McCabe'a zakazanych grafów dla programowania strukturalnego można uznać za niekompletną, przynajmniej jeśli struktury D Dijkstry są uważane za bloki konstrukcyjne.

Do 1990 roku było sporo proponowanych metod eliminowania goto z istniejących programów, przy jednoczesnym zachowaniu większości ich struktury. Różne podejścia do tego problemu proponowały również kilka pojęć równoważności, które są bardziej rygorystyczne niż po prostu równoważność Turinga, aby uniknąć wyników takich jak twierdzenie ludowe omówione powyżej. Ścisłość wybranego pojęcia równoważności dyktuje minimalny zestaw wymaganych struktur przepływu sterowania. Publikacja JACM z 1988 r. autorstwa Lyle'a Ramshawa bada pole do tego momentu, a także proponuje własną metodę. Algorytm Ramshawa był używany na przykład w niektórych dekompilatorach Javy, ponieważ kod wirtualnej maszyny Javy zawiera instrukcje rozgałęzione z celami wyrażonymi jako przesunięcia, ale wysokopoziomowy język Javy ma tylko wielopoziomowe breaki continueinstrukcje. Ammarguellat (1992) zaproponował metodę transformacji, która sięga do wymuszania pojedynczego wyjścia.

Aplikacja do Cobol

W latach 80. badacz IBM, Harlan Mills, nadzorował rozwój COBOL Structuring Facility , który stosował algorytm strukturyzacji do kodu COBOL . Transformacja Millsa obejmowała następujące kroki dla każdej procedury.

  1. Zidentyfikuj podstawowe bloki w procedurze.
  2. Przypisz unikalną etykietę do ścieżki wejściowej każdego bloku i oznacz ścieżki wyjściowe każdego bloku etykietami ścieżek wejściowych, z którymi są połączone. Użyj 0 dla powrotu z procedury i 1 dla ścieżki wejścia procedury.
  3. Podziel procedurę na jej podstawowe bloki.
  4. Dla każdego bloku, który jest miejscem docelowym tylko jednej ścieżki wyjścia, ponownie połącz ten blok z tą ścieżką wyjścia.
  5. Zadeklaruj nową zmienną w procedurze (o nazwie L dla odniesienia).
  6. Na każdej pozostałej niepołączonej ścieżce wyjściowej dodaj instrukcję, która ustawia L na wartość etykiety w tej ścieżce.
  7. Połącz powstałe programy w instrukcję wyboru, która wykonuje program z etykietą ścieżki wejściowej wskazaną przez L
  8. Skonstruuj pętlę, która wykonuje tę instrukcję wyboru, o ile L nie jest równe 0.
  9. Skonstruuj sekwencję, która inicjuje L do 1 i wykonuje pętlę.

Zauważ, że tę konstrukcję można ulepszyć, przekształcając niektóre przypadki instrukcji wyboru w podprocedury.

Zobacz też

Bibliografia

Dalsza lektura

Materiał, który nie został jeszcze omówiony powyżej: