Whiley (programovací jazyk) - Whiley (programming language) - Wikipedia

Whiley je experimentální programovací jazyk, který kombinuje funkce z funkční a rozkazovací způsob paradigmata a podporuje formální specifikace prostřednictvím funkce předpoklady, dodatečné podmínky a smyčkové invarianty.^[1] Jazyk používá psaní citlivé na tok známé také jako „tokové psaní“.

Projekt Whiley byl zahájen v roce 2009 v reakci na „Verifying Compiler Grand Challenge“, který předložil Tony Hoare v roce 2003.^[2] První veřejné vydání Whiley bylo v červnu 2010.^[3]

Whiley, který byl primárně vyvinut Davidem Pearcem, je open source projekt s příspěvky malé komunity. Systém se používá pro výzkumné projekty studentů a pro výuku vysokoškolských kurzů.^[4] To bylo podporováno v letech 2012 až 2014 z Královské společnosti novozélandského fondu Marsden.^[5]

Kompilátor Whiley generuje kód pro Virtuální stroj Java a může spolupracovat s Javou a dalšími jazyky založenými na JVM.

Přehled

Cílem Whiley je poskytnout realistický programovací jazyk, kde ověření se používá rutinně a bez přemýšlení. Myšlenka takového nástroje má dlouhou historii, ale do začátku roku 2000 byla silně prosazována Hoare Ověření velké výzvy kompilátoru. Účelem této výzvy bylo podnítit nové snahy o rozvoj a ověřování překladače, zhruba popsáno takto:^[6]

Ověřující kompilátor používá matematické a logické uvažování ke kontrole správnosti programů, které kompiluje.

— Tony Hoare

Primárním účelem takového nástroje je zlepšit kvalita softwaru zajištěním splnění programu a formální specifikace. Whiley sleduje mnoho pokusů o vývoj těchto nástrojů, včetně pozoruhodných snah jako např SPARK / Ada, ESC / Java, Spec #, Dafny, Proč3,^[7] a Frama-C.

Většina předchozích pokusů o vývoj ověřovacího kompilátoru se zaměřila na rozšíření stávajících programovacích jazyků o konstrukce pro psaní specifikací. Například, ESC / Java a Java Modeling Language přidat poznámky pro určení předpokladů a dodatečných podmínek Jáva. Rovněž, Spec # a Frama-C přidat podobné konstrukty do C# a C programovací jazyky. O těchto jazycích je však známo, že obsahují řadu funkcí, které představují pro ověřování obtížné nebo nepřekonatelné problémy.^[8] Naproti tomu jazyk Whiley byl navržen od nuly ve snaze vyhnout se běžným nástrahám a zajistit lepší ovladatelnost ověření.^[9]

Funkce

Syntaxe Whiley sleduje obecný vzhled imperativních nebo objektově orientovaných jazyků. Syntaxe odsazení je vybrána na základě použití složených závorek k vymezení bloků příkazů vzhledem k silné podobnosti Krajta. Naléhavý vzhled Whiley je však poněkud zavádějící, protože jazykové jádro je funkční a čistý.

Whiley rozlišuje a funkce (který je čistý ) z a metoda (které mohou mít vedlejší efekty ). Toto rozlišení je nezbytné, protože umožňuje použití funkcí ve specifikacích. K dispozici je známá sada primitivních datových typů, včetně bool, int, pole (např. int []) a záznamy (např. {int x, int y}). Na rozdíl od většiny programovacích jazyků je to však celočíselný datový typ, int, je neomezený a neodpovídá reprezentaci pevné šířky, například 32bitové doplněk dvou. Takže neomezené celé číslo v Whiley může nabývat jakékoli možné celočíselné hodnoty, s výhradou paměťových omezení hostitelského prostředí. Tato volba zjednodušuje ověřování, protože uvažování o modulo aritmetice je známý a těžký problém. Složené objekty (např. Pole nebo záznamy) nejsou odkazy na hodnoty na haldě, protože jsou v jazycích, jako je Jáva nebo C# ale místo toho jsou neměnný hodnoty.

Whiley používá neobvyklý přístup ke kontrole typu označovaný jako „Flow Typing“. Proměnné mohou mít různé statické typy v různých bodech funkce nebo metody. Tokové psaní je podobné psaní výskytů jak je uvedeno v Raketa.^[10] K usnadnění psaní toků podporuje Whiley unie, průsečík a typy negace.^[11] Typy Unie jsou srovnatelné s typy součtu najdete ve funkčních jazycích jako Haskell ale v Whiley nejsou disjunktní. Typy křižovatky a negace se používají v kontextu typování toku k určení typu proměnné v pravých a nepravých větvích testu typu runtime. Předpokládejme například proměnnou X typu T a test typu runtime x je S.. Na skutečné větvi typ X se stává T & S zatímco na falešné větvi se stává T &! S.

Whiley používá a strukturální spíše než nominální typový systém. Modula-3, Jít a Cejlon jsou příklady dalších jazyků, které podporují strukturální psaní v nějaké formě.

Whiley podporuje referenční životnosti podobné těm, které najdete v Rez. Při přidělování nových objektů lze uvést dobu životnosti, která označuje, kdy je možné je bezpečně uvolnit. Odkazy na takové objekty pak musí obsahovat celoživotní identifikátor, aby se zabránilo visící odkazy. Každá metoda má implicitní životnost, na kterou odkazuje tento. Proměnná typu &toto t představuje odkaz na objekt typu T který je uvolněn s uzavírací metodou. Podtypování mezi životy určuje přežívá vztah. Tím pádem, & l1: T je podtyp & l2: T pokud doživotní l1 staticky přežívá celý život l2. Život, jehož rozsah obklopuje další, jej údajně přežije. Životnosti v Whiley se liší od Rusta v tom, že v současné době neobsahují koncept vlastnictví.

Whiley nemá integrovanou podporu pro souběžnost a žádný model formální paměti, který by určoval, jak by mělo být interpretováno čtení / zápis do sdíleného proměnlivého stavu.

Příklad

Následující příklad ilustruje mnoho zajímavých funkcí v Whiley, včetně použití postconditions, invariantních smyček, invariantních typů, sjednocujících typů a typování toku. Funkce je určena k vrácení prvního indexu celého čísla položka v poli celého čísla položky. Pokud takový index neexistuje, pak nula je vrácen.

// Definujte typ přirozených číseltyp nat je (int X) kde X >= 0veřejnost funkce indexOf(int[] položky, int položka) -> (int|nula index)// Pokud se int vrátí, prvek na této pozici odpovídá položcezajišťuje index je int ==> položky[index] == položka// Pokud se int vrátí, prvek na této pozici je první shodazajišťuje index je int ==> Ne { i v 0 .. index | položky[i] == položka }// Pokud je vrácena hodnota null, žádný prvek v položkách neodpovídá položcezajišťuje index je nula ==> Ne { i v 0 .. |položky| | položky[i] == položka }:    //    nat i = 0    //    zatímco i < |položky|    // Žádný prvek dosud nebyl viděn s položkou    kde Ne { j v 0 .. i | položky[j] == položka }:        //        -li položky[i] == položka:            vrátit se i        i = i + 1    //    vrátit se nula

Ve výše uvedeném návratovém typu funkce je uveden typ sjednocení int | null což naznačuje buď an int hodnota je vrácena nebo nula je vrácen. Funkce je podmínka je vyroben ze tří zajišťuje klauzule, z nichž každá popisuje různé vlastnosti, které musí mít vrácené index. Typování toku se v těchto klauzulích používá prostřednictvím testovacího operátoru typu runtime, je. Například v první zajišťuje klauzule, proměnná index je přepsán z int | null jen int na pravé straně operátoru implikace (tj. ==>).

Výše uvedený příklad také ilustruje použití indukčního smyčka neměnná. Musí být zobrazen invariant smyčky, aby se udržel při vstupu do smyčky, pro jakoukoli danou iteraci smyčky a při ukončení smyčky. V tomto případě invariant smyčky uvádí, co je známo o prvcích položky dosud prozkoumáno - jmenovitě, že žádný z nich neodpovídá danému položka. Invariant smyčky neovlivňuje význam programu a v určitém smyslu může být považován za zbytečný. Je však vyžadován invariant smyčky, aby pomohl automatizovanému ověřovateli používajícímu v kompilátoru Whiley k prokázání, že tato funkce splňuje jeho specifikaci.

Výše uvedený příklad také definuje typ nat s příslušným zadejte invariant. Tento typ se používá k deklaraci proměnné i a naznačují, že nikdy nemůže mít zápornou hodnotu. V tomto případě deklarace zabrání potřebě další smyčky invariantní k formuláři kde i> = 0 které by jinak bylo nutné.

Dějiny

Whiley začal v roce 2009 prvním veřejným vydáním, v0.2.27 následující v červnu 2010 a v0.3.0 v září téhož roku. Jazyk se vyvíjel pomalu s mnoha syntaktickými změnami, které byly dosud provedeny. Verze předchozí v0.3.33 podporováno prvotřídní tětiva a char datové typy, ale ty byly odstraněny ve prospěch reprezentace řetězců jako omezené int [] pole. Podobně verze před v0.3.35 podporovaná prvotřídní sada (např. {int}), slovník (např. {int => bool}) a měnitelný seznam [int]), ale tyto byly zrušeny ve prospěch jednoduchých polí (např. int []). Snad nejkontroverznější bylo odstranění nemovitý datový typ ve verzi v0.3.38. Mnoho z těchto změn bylo motivováno snahou zjednodušit jazyk a zlepšit ovladatelnost vývoje kompilátoru.

Další důležitý milník ve vývoji Whiley přišel ve verzi v0.3.40 se zahrnutím referenčních životů, které vyvinul Sebastian Schweizer jako součást své Diplomová práce na University of Kaiserslautern.

Reference