Název: Soothsharp: překladač C# do jazyka Viper
Překlad názvu: Soothsharp: A C#-to-Viper translator
Autoři: Hudeček, Petr ; Parízek, Pavel (vedoucí práce) ; Ježek, Pavel (oponent)
Typ dokumentu: Diplomové práce
Rok: 2017
Jazyk: eng
Abstrakt: [eng] [cze]
Viper is a verification infrastructure developed at ETH Zurich. Using this infrastructure, programs written in the Viper language may be analyzed for correctness with respect to assertions and contracts. In this thesis, we develop a contracts library and a translator program that compiles C# code into the Viper language and thus allows it to be verified. A user may annotate their C# program with these contracts and then use the translator to determine its functional correctness. The translator supports most C# features, including types and arrays. It also integrates with Visual Studio, showing translation and verification errors to the user on-the-fly. Viper je verifikační infrastruktura vyvíjená na univerzitě ETH v Curychu. Pomocí této infrastruktury se dá ověřit, zda programy napsané v jazyku Viper vyhovují svým deklarovaným kontraktům a invariantům. V této práci vyvíjíme knihovnu kontraktů a překladač, který zkompiluje kód v jazyku C# do jazyku Viper, a tak umožní jeho verifikaci. Uživatel může anotovat svůj program těmito kontrakty a pak použít překladač, aby určil, zda je program funkčně korektní. Překladač podporuje podstatnou podmnožinu funkcí jayzku C#, včetně typů a polí. Je integrován s Visual Studiem, a ukazuje tak chyby z překladu a verifikace uživateli přímo v prostředí.
Klíčová slova: kontrakty; oprávnění; programovací jazyky; verifikace; contracts; permissions; programming languages; verification

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/90340

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-364940


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Diplomové práce