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

Re: [PVS-Help] A representation of symbols in PVS



Hello Shankar,

Thank you again for your reply...

shankar@csl.sri.com said:
> It might be useful to discuss what you're trying to formalize so that
> we can figure out a good way to achieve it.

Basically, I am defining program transformations represented as
s-expressions. Given a particular form or s-expression, I am creating
procedures to transform them to other s-expressions, as well as derive
other information and datatypes from them.

Normally, an s-expression would consist of pairs and atoms. However,
this is in a system that isn't explicitely typed. So, pairs could
contain strings, numbers, symbols, just to name a few.

I think the idea I have now which would make it most easy is something
along the lines of:

sexpr: DATATYPE
BEGIN
null: null?
symbol(value: string): symbol?
integer(value: int): integer?
pair(car:sexpr, cdr:sexpr): pari?
END sexpr