[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Prolog & PVS

Hi there!

Currently, I am working on a PVS-specification of the programming language
Prolog. For those who don't know prolog a small introduction as some basic
knowledge is necessary to understand my PVS-problem:
A (simplified) BNF-definition for prolog-terms:

  term     ::= atom | compound
  compound ::= atom(term {, term}^*)

-> an atom will be defined as an uninterpreted type.
-> a compound-term is an expression consisting of an atom followed by 1 or
     more term-arguments between '(' & ')'. (NOT to be seen as a function)

The type of a compound-term can thus be specified as a list of at least 2
items, the first being an atom, and the other(s) terms. 
How can I write down such a recursive type in PVS?

Thanks in advance to anyone!

Pieter Audenaert
Dept. Pure Mathematics,
University of Gent, Belgium