Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

Correct-by-Construction P… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

Correct-by-Construction Pretty-Printing

Paper i proceeding
Författare Nils Anders Danielsson
Publicerad i Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-Typed Programming (DTP 2013)
ISBN 978-1-4503-2384-0
Förlag Association for Computing Machinery (ACM)
Publiceringsår 2013
Publicerad vid Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU)
Språk en
Länkar dx.doi.org/10.1145/2502409.2502410
https://gup.ub.gu.se/file/126689
Ämnesord dependent types, pretty-printing
Ämneskategorier Teoretisk datalogi

Sammanfattning

A new approach to correct-by-construction pretty-printing is presented. The basic methodology is the one of classical (not necessarily correct) pretty-printing: users convert values to pretty-printer documents, and a general rendering algorithm turns documents into strings. The main novelty is that dependent types are used to ensure that, for each value, the constructed document is correct with respect to the value and a given grammar. Other parts of the development use well-established technology: the pretty-printer document interface is basically that of Wadler (2003), but with more precise types, and a single additional primitive combinator; and Wadler's rendering algorithm is used.

It is proved that if a given value is pretty-printed, and the resulting string parsed (with respect to the same, unambiguous grammar), then the original value is obtained. No guarantees are made about "prettiness".

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?