NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Head-Strictness is Not a Monotonic Abstract PropertyA property P of a language is said to be definable by abstract interpretation if there is a monotonic map abs from the domain of standard semantics to an abstract domain A of finite height, and a partition of the abstract domain into two parts A(sub p) and A(sub non p), such that any value has property P if and only if abs maps it to an element of A(sub p). Head-strictness is a property of functions over lists which asserts, roughly speaking, that whenever the function looks at the tail of a list, it looks at the head of the tail. We prove that head-strictness is not definable by abstract interpretation. We then present a non-monotonic abstract interpretation for head-strictness and prove its safety.
Document ID
19970001666
Acquisition Source
Ames Research Center
Document Type
Preprint (Draft being sent to journal)
Authors
Kamin, Samuel
(Illinois Univ. Urbana-Champaign, IL United States)
Date Acquired
August 17, 2013
Publication Date
October 18, 1991
Publication Information
Publication: NASA Review of ICLASS
Subject Category
Computer Programming And Software
Accession Number
97N70120
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
Document Inquiry

Available Downloads

There are no available downloads for this record.
No Preview Available