PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
Ruggieri S., Mesnard F. Typing linear constraints. In: ACM Transactions on Programming Languages and Systems, vol. 32 (6) article n. 21. ACM, 2010.
 
 
Abstract
(English)
We present a type system for linear constraints over the reals intended for reasoning about the input-output directionality of variables. Types model the properties of definiteness, range width or approximation, lower and upper bounds of variables in a linear constraint. Several proof procedures are presented for inferring the type of a variable and for checking validity of type assertions. We rely on theory and tools for linear programming problems, linear algebra, parameterized polyhedra and negative constraints. An application of the type system is proposed in the context of the static analysis of constraint logic programs. Type assertions are at the basis of the extension of wellmoding from pure logic programming. The proof procedures (both for type assertion validity and for well-moding) are implemented and their computational complexity is discussed. We report experimental results demonstrating the efficiency in practice of the proposed approach.
URL: http://dl.acm.org/citation.cfm?id=1749610&CFID=68484065&CFTOKEN=47830451
DOI: 10.1145/1749608.1749610
Subject Languages
Verification
Linear constraints
Polyhedra
Constraint logic programming
Well-moding
Definiteness
I.2.2 Automatic Programming
I.2.3 Deduction and Theorem Proving


Icona documento 1) Download Document PDF


Icona documento Open access Icona documento Restricted Icona documento Private

 


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional