Filozofia inżynierska: Barbara Liskov, kontrakt jest typem

Najważniejsze wnioski
- Abstrakcja dotyczy zachowania, nie struktury. Typ to kontrakt, którego dotrzymuje — operacje i ich znaczenie — a nie bity, które przechowuje. Korzysta się z danej rzeczy poprzez jej obietnice, nigdy poprzez jej reprezentację.
- Podtyp musi honorować obietnice nadtypu. Zasada podstawienia Liskov: wszędzie tam, gdzie oczekiwany jest nadtyp, podtyp musi działać bez naruszania założeń wywołującego — słabsze warunki wstępne, silniejsze warunki końcowe, zachowane niezmienniki.
- Modularność oznacza rozumowanie o części bez całości. Precyzyjna definicja Liskov: można zrozumieć i zweryfikować moduł w izolacji, ufając, że jego zależności dotrzymają swoich kontraktów. Abstrakcja jest tym, co czyni to zaufanie zasadnym.
- Uczyniła abstrakcję danych prymitywem programistycznym. Od CLU przez Argus aż po Nagrodę Turinga z 2008 roku jedna idea skaluje się od struktury danych po rozproszoną bazę danych: zdefiniuj kontrakt, ukryj mechanizm.
Zasada
„Niech φ(x) będzie własnością dowodliwą dla obiektów x typu T. Wówczas φ(y) powinno być prawdziwe dla obiektów y typu S, gdzie S jest podtypem T.” — Barbara Liskov i Jeannette Wing1
Czytane powoli, jest to formalne sformułowanie tego, co dziedzina nazywa dziś zasadą podstawienia Liskov, pochodzące z jej pracy z 1994 roku napisanej wspólnie z Jeannette Wing.1 Po odarciu z notacji mówi ono coś niemal surowego: podtyp nie ma prawa zaskakiwać. Wszystko, co można udowodnić jako prawdziwe dla nadtypu, musi pozostać prawdziwe, gdy przekaże się programowi podtyp w jego miejsce. Podtyp dziedziczy obietnice rodzica, a nie tylko jego kształt — i jeśli nie potrafi dotrzymać tych obietnic, nie jest podtypem, bez względu na to, co twierdzi mechanizm sprawdzania typów.
Za tą surowością kryje się zwieńczenie jednej idei, którą Liskov zgłębiała przez czterdzieści lat: typ jest definiowany przez swoje zachowanie, a nie przez swoją reprezentację. Moduł to kontrakt — zbiór operacji o określonym znaczeniu — a cały sens kontraktu polega na tym, że można korzystać z danej rzeczy bez czytania, jak została zbudowana. Zastępowalność to po prostu to samo przekonanie zastosowane do dziedziczenia: jeśli S twierdzi, że jest rodzajem T, to wszędzie tam, gdzie obiecano T, S musi honorować tę samą obietnicę. Struktura może się różnić. Zachowanie — nie.
To, dlaczego ma to znaczenie, jest nicią przewodnią całej jej kariery: duże programy daje się ogarnąć tylko wtedy, gdy można rozumować o jednej części bez trzymania całości w głowie. Liskov nazywała to modularnością i rozumiała przez to coś precyzyjnego: zdolność rozumienia i weryfikowania modułu w izolacji, w zaufaniu, że wszystko, od czego on zależy, dotrzyma swojego deklarowanego kontraktu. Abstrakcja danych jest tym, co czyni to zaufanie zasadnym, a behawioralne podtypowanie tym, co nie pozwala dziedziczeniu po cichu go złamać. To samo przekonanie leży u podstaw argumentu, że dobre systemy buduje się tak, aby gust był technicznym systemem, który można zbadać — kontraktem, który można sformułować i sprawdzić — a nie tradycją wchłanianą przez czytanie całej bazy kodu.
Kontekst
Barbara Jane Huberman Liskov urodziła się 7 listopada 1939 roku w Los Angeles w Kalifornii.2 Stopień licencjata z matematyki, ze specjalizacją poboczną z fizyki, uzyskała na Uniwersytecie Kalifornijskim w Berkeley w 1961 roku.2 Gdy aplikowała na studia doktoranckie z matematyki w Berkeley i Princeton, Princeton w ogóle nie przyjmowało kobiet; zamiast tego podjęła pracę i niemal przypadkiem trafiła do wczesnej informatyki, programując w Mitre Corporation oraz na Harvardzie, zanim ostatecznie zdecydowała, że jednak chce doktoratu.2
Doktorat uzyskała na Uniwersytecie Stanforda w 1968 roku — jako jedna z pierwszych kobiet w Stanach Zjednoczonych, które otrzymały stopień doktora z wydziału informatyki.2 Jej promotorem był John McCarthy, twórca języka Lisp i jeden z założycieli dziedziny sztucznej inteligencji; jej rozprawa doktorska opierała się na programie grającym końcówki szachowe, a przy okazji opracowała heurystykę zabójcy (killer heuristic), sztuczkę porządkowania ruchów wciąż stosowaną w przeszukiwaniu drzewa gry.2 Ten szczegół warto zapamiętać: wyrosła ze sztucznej inteligencji, pod okiem człowieka, który ukuł to pojęcie, a następnie odwróciła się od niej ku problemowi, który miał ją zdefiniować — nie jak sprawić, by maszyna myślała, ale jak sprawić, by duży program był zrozumiały.

Po Stanfordzie wróciła do Mitre, gdzie kierowała projektowaniem systemu operacyjnego Venus — niewielkiego, taniego, interaktywnego systemu z podziałem czasu, zbudowanego, by zbadać, jak staranna architektura maszyny i oprogramowania może uprościć system.23 W 1972 roku dołączyła do kadry MIT, gdzie pozostaje do dziś, obecnie jako Institute Professor — najwyższa ranga nadawana przez tę instytucję.2 Venus nauczył ją pytania. Niepokój związany z kryzysem oprogramowania we wczesnych latach 70. — budzące się uświadomienie, że programy stały się zbyt duże, by ktokolwiek mógł o nich rozumować — to pytanie wyostrzył. Odpowiedzią stało się CLU.
Praca
Abstrakcja danych i język CLU
Począwszy od 1973 roku Liskov i jej studenci na MIT zaprojektowali i zbudowali CLU, jeden z najbardziej dyskretnie wpływowych języków, jakie kiedykolwiek powstały — język, w którym niemal nikt nie pisał kodu produkcyjnego, a którego idee są dziś niemal we wszystkim.4 Jego organizującym pojęciem był cluster, od którego język bierze swą nazwę: jednostka, która łączy reprezentację danych z dozwolonymi na niej operacjami i całkowicie ukrywa tę reprezentację za owym zbiorem operacji.4 Cluster był konkretnym urzeczywistnieniem abstrakcyjnego typu danych — idei, że typ powinien być znany użytkownikom wyłącznie przez to, co robi, nigdy przez to, jak przechowuje swoje bity.45
CLU na tym nie poprzestał. Zapoczątkował lub spopularyzował niezwykły zestaw cech, które dziś są standardem: iteratory, zaimplementowane jako korutyny z instrukcją yield, dzięki czemu można było przejść przez kolekcję bez odsłaniania jej wewnętrznej struktury; strukturalną obsługę wyjątków z signal i except, traktowaną jako część normalnego przepływu sterowania, a nie jako coś doczepionego; polimorfizm parametryczny — bezpieczne typowo typy parametryzowane z ograniczeniami, przodek typów generycznych; bezpieczne typowo typy wariantowe; oraz wielokrotne wartości zwracane poprzez przypisanie równoległe.4 Iteratory pojawiły się ponownie w Python, C# i Ruby. Typy parametryzowane stały się typami generycznymi w Javie i C#. Obsługa wyjątków ukształtowała Javę i C++. Projektanci Swifta wymienili CLU z nazwy.4 Język był bankiem nasion.
Ale cechy były wtórne wobec zasady. Liskov dowodziła, że abstrakcja jest mechanizmem, za pomocą którego zarządzamy złożonością — trudną rzecz buduje się, definiując czystą granicę, określając, co przez nią przechodzi, a następnie nigdy nie musząc myśleć o obu stronach naraz. CLU był dowodem na to, że język programowania może egzekwować tę granicę, a nie jedynie ją dopuszczać. Kompilator stał się sprzymierzeńcem kontraktu.
Zasada podstawienia Liskov
W 1987 roku Liskov wygłosiła na konferencji OOPSLA wykład programowy zatytułowany „Data Abstraction and Hierarchy”, opublikowany rok później w SIGPLAN Notices.6 Programowanie obiektowe było wówczas na fali wznoszącej, a wraz z nim idea podtypów — typów, które dziedziczą po innych typach i je rozszerzają. Liskov postawiła oczywiste pytanie, którego nikt nie sformułował precyzyjnie: kiedy w istocie bezpiecznie jest traktować podtyp jak jego nadtyp? Jej odpowiedzią, słowami samego wykładu, była własność podstawienia: „Tym, czego tu się oczekuje, jest coś w rodzaju następującej własności podstawienia: jeśli dla każdego obiektu o1 typu S istnieje obiekt o2 typu T taki, że dla wszystkich programów P zdefiniowanych w kategoriach T zachowanie P pozostaje niezmienione, gdy o1 zostanie podstawione za o2, to S jest podtypem T.”6
Popularna parafraza, którą można spotkać wszędzie — „jeśli S jest podtypem T, to obiekty typu T mogą być zastąpione obiektami typu S bez zmiany żadnej z pożądanych własności programu” — jest wiernym skróceniem tamtego sformułowania.7 W 1994 roku Liskov i Jeannette Wing nadały temu rygor w pracy „A Behavioral Notion of Subtyping”, podając warunki, które musi spełnić prawdziwy podtyp: jego metody muszą wymagać nie więcej (słabsze lub równe warunki wstępne) i obiecywać nie mniej (silniejsze lub równe warunki końcowe) niż metody nadtypu, a sam podtyp musi zachowywać niezmienniki i własności historyczne nadtypu.1 Te warunki, wzięte łącznie, są tym, czym jest behawioralne podtypowanie — i są też powodem, dla którego potoczne sformułowania w stylu „jeśli wygląda jak kaczka i kwacze jak kaczka” nie pochodzą od niej i chybiają sedna: wyglądanie i kwakanie to kształt; zasada dotyczy dotrzymanych obietnic.
Klasycznym kontrprzykładem jest kwadrat, który dziedziczy po prostokącie. Klasa Rectangle pozwala ustawiać szerokość i wysokość niezależnie; klient może ustawić wysokość i zaufać, że szerokość pozostanie niezmieniona. Klasa Square, która po niej dziedziczy, musi wymusić równość obu wartości — więc ustawienie wysokości po cichu zmienia szerokość, a rozsądne założenie klienta zostaje naruszone.7 Kwadrat jest prostokątem w słownikowym sensie i przechodzi każde sprawdzenie typów, a mimo to nie jest behawioralnym podtypem, ponieważ nie potrafi dotrzymać obietnic prostokąta. Cała lekcja zawiera się w tym jednym kształcie: dziedziczenie struktury nie jest dziedziczeniem kontraktu.
Systemy rozproszone: Argus i Thor
Liskov nie pozostała przy projektowaniu języków. We wczesnych latach 80. zbudowała Argus, opisywany jako pierwszy język wysokiego poziomu wspierający implementację programów rozproszonych — programów rozsianych po maszynach, które ulegają awariom niezależnie od siebie.23 Argus, rozszerzenie CLU, wprowadził strażników (guardians — obiekty, które enkapsulują stan rozproszony, dostępne przez handlery) oraz akcje atomowe (transakcje, które albo kończą się w całości, albo wcale, nawet w obliczu awarii, koordynowane przez dwufazowe zatwierdzanie), a także zademonstrował potokowanie obietnic (promise pipelining), gdzie można wystawić wywołanie i kontynuować pracę, zanim wróci jego wynik.9 Trudnym problemem rozproszenia jest awaria częściowa — jeden węzeł umiera, gdy pozostałe żyją — a Argus skierował przeciw niej abstrakcję danych: strażnik to kontrakt, który obowiązuje nawet wtedy, gdy sieć nie obowiązuje.
Thor, w latach 90., był rozproszoną obiektową bazą danych, zapewniającą niezawodne, wysoce dostępne trwałe przechowywanie obiektów, do których uzyskiwały dostęp programy napisane w wielu językach.23 Nić przewodnia od CLU jest dokładna. Cluster ukrywa reprezentację za operacjami; strażnik ukrywa stan rozproszony za operacjami atomowymi; obiekt Thora ukrywa trwałość za typowanym interfejsem. W każdej skali — struktura danych, usługa sieciowa, baza danych — ruch Liskov jest ten sam: zdefiniuj kontrakt, ukryj mechanizm i pozwól reszcie systemu rozumować wyłącznie o kontrakcie.

Nagroda Turinga z 2008 roku i dziedzictwo
W 2009 roku ACM przyznało Liskov Nagrodę Turinga A.M. za rok 2008 — najwyższe wyróżnienie w informatyce — z uzasadnieniem: „Za wkład w praktyczne i teoretyczne podstawy projektowania języków programowania i systemów, w szczególności w zakresie abstrakcji danych, odporności na awarie oraz przetwarzania rozproszonego.”8 Rozszerzone uzasadnienie precyzyjnie nazywa nić przewodnią: rozwinęła „abstrakcję danych, modularność, odporność na awarie, trwałość oraz systemy przetwarzania rozproszonego.”8 Wcześniej otrzymała już Medal Johna von Neumanna IEEE w 2004 roku „za fundamentalny wkład w języki programowania, metodologię programowania i systemy rozproszone”, a później została wprowadzona do National Inventors Hall of Fame (2012) i uhonorowana Medalem Benjamina Franklina (2023).2
Dziedzictwo nie jest językiem ani systemem, który można wskazać i uruchomić. Polega ono na tym, że sposób, w jaki pracujący programiści myślą dziś — „programuj pod interfejs”, „polegaj na kontraktach, nie na implementacjach”, „ta klasa narusza LSP” — to słownik Liskov, wchłonięty tak całkowicie, że większość ludzi, którzy go używają, nigdy nie przeczytała tej pracy. To najgłębszy rodzaj wpływu: gdy twoja idea przestaje być przypisywana, ponieważ stała się powietrzem.
Metoda
Metoda jest spójna na przestrzeni trzydziestu lat — systemy operacyjne, projektowanie języków i rozproszone bazy danych.
Definiuj typ przez jego zachowanie, nie przez jego reprezentację. Powracającym ruchem jest wykreślenie granicy, dokładne określenie, co przez nią przechodzi, a następnie odmowa dopuszczenia, by którakolwiek strona zależała od wnętrzności drugiej. Cluster, strażnik, obiekt Thora to wszystko ten sam akt: kontrakt, który ukrywa mechanizm.45
Uczyń modularność dosłowną, a potem ją egzekwuj. Modularność dla Liskov nie jest preferencją w organizacji kodu — to zdolność rozumowania o module w izolacji, w zaufaniu, że jego zależności dotrzymają swoich kontraktów. Kompilator CLU egzekwował barierę abstrakcji, a nie jedynie grzecznie ją sugerował. Dyscyplina jest realna tylko wtedy, gdy narzędzie ją sprawdza.4
Podtyp musi dotrzymać obietnic nadtypu. Behawioralne podtypowanie to zasada, że dziedziczenie jest kontraktem, a nie wygodą. Słabsze warunki wstępne, silniejsze warunki końcowe, zachowane niezmienniki — podtyp może robić więcej, ale nigdy nie może wymagać więcej ani obiecywać mniej niż jego nadtyp.1
Atakuj trudny problem na granicy. Awaria częściowa w systemach rozproszonych jest brutalna właśnie dlatego, że niszczy zdolność rozumowania lokalnego. Odpowiedzią Argusa było wepchnięcie abstrakcji w sam model awarii — akcje atomowe i strażnicy — tak by programista wciąż mógł rozumować o danej części bez symulowania każdego sposobu, w jaki sieć mogłaby się rozpaść.23
Przenoś jedną ideę aż do samej góry. Abstrakcja danych w skali stosu, usługi sieciowej i bazy danych jest rozpoznawalnie tą samą ideą. Liskov nie wymyślała nowej filozofii dla każdej dziedziny; znalazła tę, która się skalowała, i niosła ją od systemu typów z lat 70. po rozproszony magazyn z lat 90.
Łańcuch wpływów
Kto ją ukształtował
John McCarthy. Jej promotor doktorski na Stanfordzie, twórca języka Lisp i założyciel dziedziny sztucznej inteligencji, dał jej zarówno rygor matematycznej informatyki, jak i — poprzez jej odwrót od sztucznej inteligencji ku strukturze programów — problem, który stał się dziełem jej życia.2 (Wpływ bezpośredni)
Kryzys oprogramowania i epoka programowania strukturalnego. Liskov dojrzewała jako badaczka dokładnie wtedy, gdy dziedzina przyznała, że programy przerosły ludzkie pojmowanie. Ruch programowania strukturalnego — Dijkstra, Hoare, Wirth — dowodził, że przepływ sterowania musi być zdyscyplinowany, by można było o nim rozumować. Liskov rozszerzyła to samo przekonanie na dane: nie wystarczy zdyscyplinować, jak program się porusza; trzeba zdyscyplinować, co znaczą jego dane i komu wolno widzieć, jak są przechowywane. (Wpływ formacyjny)
C.A.R. Hoare i dyscyplina specyfikacji. Prace Hoare’a nad warunkami wstępnymi, warunkami końcowymi i niezmiennikami — rozumowaniem o programach jako logicznych asercjach — są bezpośrednim intelektualnym przodkiem warunków behawioralnego podtypowania, które ona i Wing sprecyzowały. (Wpływ formacyjny)
Kogo ukształtowała
Każdy nowoczesny system typów. Typy generyczne w Javie i C#, iteratory w Python i C#, obsługa wyjątków w całej rodzinie języków C, projekt Swifta — cechy, które zapoczątkował CLU, są dziś domyślnym wyposażeniem niemal każdego języka.4
Praktyka obiektowa. „Programuj pod interfejs, nie pod implementację”, odwrócenie zależności i całe „L” ze słownika SOLID to zasada Liskov, doprowadzona do postaci operacyjnej. Całe pokolenie nauczyło się rozpoznawać złą podklasę, nigdy nie dowiadując się, czyj to był pomysł.7
Inżynieria systemów rozproszonych. Akcje atomowe, gwarancje transakcyjne między ulegającymi awariom węzłami oraz praktyka traktowania zdalnej usługi jako kontraktu, który przetrwa awarię częściową, prowadzą wstecz przez Argus i Thor.23
Nić przewodnia
Edsger Dijkstra dowodził, że program musi być ustrukturyzowany tak, by człowiek mógł o nim rozumować — programowanie strukturalne było dyscypliną przepływu sterowania w służbie poprawności. Liskov to bezpośrednia linia rodowa: zrobiła dla danych to, co Dijkstra zrobił dla sterowania, obstając przy tym, że modularne rozumowanie wymaga zdyscyplinowanych barier abstrakcji, a nie tylko zdyscyplinowanych pętli. A tam, gdzie Thompson i Ritchie zbudowali Uniksa i C wokół małych komponentów, które „robią jedną rzecz dobrze” i komponują się przez czyste interfejsy, Liskov dała teorię dlaczego ta kompozycja jest godna zaufania: komponent, na którym można polegać, to taki, którego kontrakt można sformułować i którego podtypy go honorują. Nawet kompilator Grace Hopper był aktem abstrakcji — przeniesieniem tłumaczenia do maszyny, by człowiek mógł rozumować we własnych kategoriach; Liskov uczyniła samą abstrakcję jednostką projektowania programu, a nie wygodą dostarczaną przez kompilator. (Pomost serii)
Co z tego biorę
Lekcja, którą zachowuję, brzmi: interfejs jest obietnicą, a jedyne interfejsy warte czegokolwiek to te, których faktycznie się dotrzymuje. Łatwo jest napisać sygnaturę typu; trudno jest uhonorować wszystko, co ta sygnatura implikuje, i nigdy po cichu jej nie naruszyć przy nowej podklasie czy refaktoryzacji. Zasada Liskov to standard, do którego przykładam granicę: nie „czy sprawdzenie typów przechodzi?”, lecz „czy wywołujący może zaufać tej rzeczy wszędzie tam, gdzie zaufano jej rodzicowi, bez czytania, jak została zbudowana?”. To ta sama poprzeczka, co jakość będąca jedyną zmienną — pytaniem nigdy nie jest, czy kod się kompiluje, lecz czy kontrakt jest realny.
W świecie, w którym teraz buduję — agenty, pętle narzędziowe, systemy AI — przekonanie Liskov jest bardziej nośne niż kiedykolwiek, ponieważ komponenty, które komponuję, są z natury nieprzejrzyste. Narzędzie, podagent, wywołanie modelu to moduł: wywołuje się go na podstawie kontraktu i nie można odczytać jego wnętrzności. Cała gra polega na tym, czy ten kontrakt się utrzyma — czy narzędzie, które twierdzi, że „przeszukuje bazę kodu”, faktycznie zwraca to, co obiecała jego specyfikacja, czy też podmiana jednego modelu na inny po cichu osłabia warunek końcowy, na którym opierała się reszta systemu. To zasada podstawienia Liskov w stroju z 2026 roku: podstawiony komponent musi dotrzymać obietnic tego, który zastąpił. Dyscyplina formułowania kontraktów i sprawdzania, czy podtypy je honorują, to dokładnie ta sama dyscyplina, która sprawia, że bramka dowodowa jest czymś więcej niż hasłem — systemem, o którym można rozumować w częściach, ponieważ każda część dotrzymuje słowa.
FAQ
Na czym polega filozofia inżynierska Barbary Liskov?
Podstawowym przekonaniem Liskov jest to, że typ definiuje się przez jego zachowanie, a nie przez jego reprezentację, i że właśnie to sprawia, że duże programy daje się ogarnąć. Moduł to kontrakt — zbiór operacji o określonym znaczeniu — a celem kontraktu jest to, że można korzystać z modułu bez rozumienia, jak został zbudowany. Ta idea abstrakcji danych przewija się przez wszystko, co zbudowała, od języka CLU po system rozproszony Argus, i zaowocowała jej najsłynniejszym wynikiem: zasadą, że podtyp musi honorować każdą obietnicę składaną przez swój nadtyp.451
Czym jest zasada podstawienia Liskov?
To wymóg, by podtyp był użyteczny wszędzie tam, gdzie oczekiwany jest jego nadtyp, bez naruszania założeń wywołującego. Formalnie, w sformułowaniu Liskov i Wing z 1994 roku: „Niech φ(x) będzie własnością dowodliwą dla obiektów x typu T. Wówczas φ(y) powinno być prawdziwe dla obiektów y typu S, gdzie S jest podtypem T.”1 W swoim wykładzie programowym na OOPSLA w 1987 roku ujęła to jako własność podstawienia: jeśli podstawienie obiektu typu S za obiekt typu T pozostawia zachowanie każdego programu niezmienionym, to S jest podtypem T.6 W praktyce prawdziwy podtyp musi wymagać nie więcej niż jego nadtyp (słabsze lub równe warunki wstępne), obiecywać nie mniej (silniejsze lub równe warunki końcowe) i zachowywać jego niezmienniki. Popularne sformułowania w stylu „jeśli wygląda jak kaczka” nie pochodzą od Liskov i chybiają sedna: zasada dotyczy dotrzymanych obietnic, a nie powierzchownego podobieństwa.7
Co wynalazła Barbara Liskov?
Zaprojektowała i poprowadziła implementację języka programowania CLU (rozpoczętego w 1973 roku), który wprowadził lub spopularyzował abstrakcyjne typy danych, iteratory, strukturalną obsługę wyjątków oraz polimorfizm parametryczny — cechy dziś standardowe w Javie, C#, Python, Swift i innych.4 Wcześniej zbudowała system operacyjny z podziałem czasu Venus; później stworzyła Argus, pierwszy język wysokiego poziomu dla programów rozproszonych, oraz Thor, rozproszoną obiektową bazę danych.23 Wspólnie z Jeannette Wing sformalizowała behawioralne podtypowanie, nazywane dziś zasadą podstawienia Liskov.1
Dlaczego Barbara Liskov otrzymała Nagrodę Turinga?
ACM przyznało jej Nagrodę Turinga A.M. za rok 2008 „za wkład w praktyczne i teoretyczne podstawy projektowania języków programowania i systemów, w szczególności w zakresie abstrakcji danych, odporności na awarie oraz przetwarzania rozproszonego.”8 Wyróżnienie obejmuje całą jej karierę: uczynienie abstrakcji danych prymitywem języka programowania poprzez CLU, rozwinięcie modularności i teorii podtypowania oraz skierowanie tych idei przeciw trudnemu problemowi budowy niezawodnych systemów na maszynach, które ulegają awariom niezależnie od siebie. Była jedną z pierwszych kobiet w USA, które uzyskały doktorat z informatyki (Stanford, 1968), i jest Institute Professor na MIT.2
Źródła
-
Barbara H. Liskov i Jeannette M. Wing, „A Behavioral Notion of Subtyping,” ACM Transactions on Programming Languages and Systems 16, nr 6 (listopad 1994): 1811–1841. Wymóg podtypu: „Niech φ(x) będzie własnością dowodliwą dla obiektów x typu T. Wówczas φ(y) powinno być prawdziwe dla obiektów y typu S, gdzie S jest podtypem T.” Warunki: metody o słabszych lub równych warunkach wstępnych i silniejszych lub równych warunkach końcowych, zachowane niezmienniki i własności historyczne. Wydawca rejestrujący (DOI): 10.1145/197320.197383. ↩↩↩↩↩↩↩
-
„Barbara Liskov,” Wikipedia. Urodzona 7 listopada 1939 w Los Angeles; licencjat z matematyki (specjalizacja poboczna z fizyki), UC Berkeley, 1961; doktorat, Stanford, 1968, promotor John McCarthy, na temat programów grających końcówki szachowe (heurystyka zabójcy); jedna z pierwszych Amerykanek z doktoratem z informatyki. System operacyjny Venus w Mitre; CLU; Argus („pierwszy język wysokiego poziomu wspierający implementację programów rozproszonych”, z potokowaniem obietnic); obiektowa baza danych Thor; Institute Professor na MIT. Medal Johna von Neumanna IEEE (2004); National Inventors Hall of Fame (2012); Medal Benjamina Franklina (2023). ↩↩↩↩↩↩↩↩↩↩↩↩↩↩↩
-
„Barbara Liskov,” Encyclopaedia Britannica. System z podziałem czasu Venus; CLU i abstrakcja danych; programowanie rozproszone Argus; rozproszona obiektowa baza danych Thor; Nagroda Turinga z 2008 roku. ↩↩↩↩↩↩
-
„CLU (programming language),” Wikipedia. Zaprojektowany przez Barbarę Liskov i studentów na MIT, rozpoczęty w 1973 roku, po raz pierwszy pojawił się w 1975. Clustery (mechanizm rozszerzania typów / abstrakcyjnego typu danych); iteratory poprzez korutyny
yield; obsługa wyjątkówsignal/except; bezpieczne typowo typy parametryzowane (polimorfizm parametryczny) i typy wariantowe; wielokrotne wartości zwracane. Wpłynął na typy generyczne i iteratory w Javie, C#, Python, Ruby i został wymieniony przez projektantów Swifta. ↩↩↩↩↩↩↩↩↩↩ -
Barbara Liskov i Stephen Zilles, „Programming with Abstract Data Types,” Proceedings of the ACM SIGPLAN Symposium on Very High Level Languages, 1974. Fundamentalna praca wprowadzająca podejście abstrakcyjnego typu danych, które zaimplementował CLU. Zobacz także retrospektywny wykład Liskov „The Power of Abstraction” (OOPSLA, 2009). ↩↩↩
-
Barbara Liskov, „Keynote address – data abstraction and hierarchy,” ACM SIGPLAN Notices 23, nr 5 (maj 1988): 17–34, z dodatku do materiałów OOPSLA ‘87. Oryginalna własność podstawienia: „Tym, czego tu się oczekuje, jest coś w rodzaju następującej własności podstawienia: jeśli dla każdego obiektu o1 typu S istnieje obiekt o2 typu T taki, że dla wszystkich programów P zdefiniowanych w kategoriach T zachowanie P pozostaje niezmienione, gdy o1 zostanie podstawione za o2, to S jest podtypem T.” ↩↩↩
-
„Liskov substitution principle,” Wikipedia. Początek w wykładzie programowym Liskov z 1987 roku i formalizacji Liskov–Wing z 1994 roku; popularna parafraza „obiekty nadklasy mogą być zastąpione obiektami podklasy bez psucia programu”; warunki behawioralnego podtypowania; naruszenie prostokąt/kwadrat jako kanoniczny kontrprzykład. Sformułowania w stylu „kaczego typowania” nie pochodzą od Liskov. ↩↩↩↩
-
„Barbara Liskov – A.M. Turing Award Laureate,” ACM. Uzasadnienie Nagrody Turinga za rok 2008: „Za wkład w praktyczne i teoretyczne podstawy projektowania języków programowania i systemów, w szczególności w zakresie abstrakcji danych, odporności na awarie oraz przetwarzania rozproszonego.” Ogłoszenie i rozszerzone uzasadnienie („abstrakcja danych, modularność, odporność na awarie, trwałość oraz systemy przetwarzania rozproszonego”): CRA-WP. ↩↩↩
-
Barbara Liskov, „Distributed Programming in Argus,” Communications of the ACM 31, nr 3 (marzec 1988): 300–312. Argus jako rozszerzenie CLU dla programów rozproszonych; strażnicy (obiekty enkapsulujące stan rozproszony, dostępne przez handlery); akcje atomowe ze ścisłymi gwarancjami spójności i atomowości koordynowane przez dwufazowe zatwierdzanie; zagnieżdżone transakcje rozproszone. Zobacz także „Guardians and Actions: Linguistic Support for Robust, Distributed Programs” (Liskov i Scheifler, 1983). ↩