plspec - A Specification Language for Prolog Data


In general, even though Prolog is a dynamically typed language, predicates may not be called with arbitrarily typed arguments. Assumptions regarding type or mode are often made implicitly, without being directly represented in the source code. This complicates identifying the types or data structures anticipated by predicates. In consequence, Covington et al. proposed that Prolog developers should implement their own runtime type checking system. In this paper, we present a re-usable Prolog library named plspec. It offers a simple and easily extensible DSL used to specify type and structure of input and output arguments. Additionally, an elegant insertion of multiple kinds of runtime checks was made possible by using Prolog language features such as co-routining and term expansion. Furthermore, we will discuss performance impacts and possible future usage of these annotations.

In Proceedings Conference on Declarative Programming (DECLARE 2017), Springer LNCS
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.