Search results for keyword `valid'

[69]

Don Batory and Bart J. Geraci. Validating component compositions in software system generators. In International Conference on Software Reuse, Florida, 1996. (PostScript)

Generators synthesize software systems by composing components from reuse libraries. In general, not all syntactically correct compositions are semantically correct. In this paper, we present domain-independent algorithms for the GenVoca model of software generators to validate component compositions. Our work relies on attribute grammars and offers powerful debugging capabilities with explanation-based error reporting. We illustrate our approach by showing how compositions are debugged by a GenVoca generator for container data structures.

[136]

Pascal Chambre. Contribution à la validation de programmes concurrents avec contraintes. PhD thesis, Orléans-LIFO, 1997.

[147]

Laurian M. Chirica and David F. Martin. Toward compiler implementation correctness proofs. ACM Trans. Progr. Languages and Systems, 8(2):185-214, April 1986.

[148]

Laurian M. Chirica. Contributions to Compiler Correctness. Ph.D. thesis, Comp. Sc. Department, University of California, Los Angeles, CA, October 1976.

[166]

Bruno Courcelle and Pierre Deransart. Proofs of partial correctness for attribute grammars with application to recursive procedures and logic programming. Information and Computation, 78(1):1-55, July 1988.

[171]

Bruno Courcelle. Attribute grammars: Definitions, analysis of dependencies, proof methods. In Bernard Lorho, editor, Methods and Tools for Compiler Construction, pages 81-102. Cambridge University Press, New York, New York, 1984.

[194]

Pierre Deransart. Description par attributs sémantiques de lisp pur et preuve de l'équivalence de la définition traductive et de l'évaluateur. rapport de recherche 220, IRIA-Laboria, Rocquencourt, March 1977.

[195]

Pierre Deransart. Preuve et génération d'attributs sémantiques. In Coll. AFCET ``Théorie et Techniques de l'Informatique'', Vol. 1, pages 412-422. Gif-sur-Yvette, November 1978. See also: rapport de recherche 302, IRIA-Laboria, Rocquencourt (May 1978).

[196]

Pierre Deransart. Proof and synthesis of semantic attributes in compiler definition. rapport de recherche 333, IRIA-Laboria, Rocquencourt, December 1978.

[197]

Pierre Deransart. Technique de preuve par attributs appliquée à un compilateur lisp. rapport de recherche 271, IRIA-Laboria, Rocquencourt, January 1978.

[198]

Pierre Deransart. Proof by semantic attributes of a lisp compiler. The Computer Journal, 22(3):240-245, August 1979.

[199]

Pierre Deransart. Synthèse automatique de traductions définies par attributs sémantiques. In 2ème Congrès AFCET-INRIA ``Reconnaissance des Formes et Intelligence Artificielle'', Vol. 1, pages 111-120. Toulouse, September 1979.

[200]

Pierre Deransart. Logical attribute grammars. In R. E. A. Mason, editor, Information Processing '83, pages 463-469. North-Holland, Amsterdam, September 1983. Paris.

[201]

Pierre Deransart. Validation des grammaires d'attributs. thèse d'état, University de Bordeaux I, October 1984.

[324]

Harald Ganzinger. Deriving proof rules for programming language constructs from static and dynamic attribute structures. ??unknown reference??, August 1977.

[382]

Gorel Hedin, Lennart Ohlsson, and John McKenna. Product configuration using object oriented grammars. In 8th International Symposium on System Configuration Management (SCM-8), Brussels, July 1998. (co-located with ECOOP'98).

This paper presents a technique for product configuration modelling based on object-orientation and attribute grammars. The technique allows efficient interactive configurator tools to be generated for specified product families. Additional benefits include a high degree of checkability, early validation, readability, and reusability. The mechanical configuration of plate heat exchangers is used to demonstrate these benefit

[430]

N. Iwamoto. Relational attribute grammars. M. eng. thesis, Department of Comp. Sc., Yamanashi University, 1985. (in Japanese).

[526]

Takuya Katayama and Yutaka Hoshino. Verification of attribute grammars. In 8th ACM Symp. on Principles of Progr. Languages, pages 177-186. ACM press, Williamsburg, VA, January 1981.

[581]

R. Krishnaswamy and A. B. Pyster. On the correctness of semantic-syntax-directed translations. J. ACM, 27(2):338-355, April 1980.

[650]

P. M. Lu, S. S. Yau, and W. Hong. A formal methodology using attributed grammars for multiprocessing-system software development. Information Sciences. An International Journal, 30(2 and 3):79-105 and 107-123, 1983. I: Design Representation, II: Validation.

[735]

Anne Neirynck. Static analysis of aliases and side effects in higher-order languages. Technical Report TR88-896, Cornell University, Computer Science Department, February 1988.

In recent years, there has been substantial interest in the development of programming languages for new parallel architectures. A basic design conflict arises because languages with simple semantics tend to use storage inefficiently, whereas languages allowing the programmer to access storage explicitly are difficult to analyze. We present a compile-time estimation scheme for determining whether an expression in an imperative language either uses or updates the store. We also determine the aliasing behavior of expressions and in general, we can tell whether the evaluation of two expressions interfere. Current interprocedural dataflow techniques for aliasing and side effect inference are valid for first-order languages. Our inference schemes provide information about aliasing and side effects in a higher-order expression language with call-by-value semantics. The higher order character of the language represents only a partial obstacle. On the other hand, the presence of l-valued expressions has the consequence that aliasing information must be computed for all expressions, and cannot be represented as a relation among identifiers. Furthermore, the introduction of pointers make aliasing and side effects flow-dependent properties. Abstract interpretation techniques allow us to define compositional static inference schemes for aliasing and side effects, which can be proved sound with respect to the standard semantics by structural induction. The abstract interpretation functions are easy to modify, in case a different type of information is requested. We also discuss how different language features may affect the static analyses, simplifying them or making them untractable. The abstract interpretation functions implicitly define static inference algorithms, which can easily be implemented by an attribute grammar, or any other tool capable of performing computations on the abstract syntax tree. The accuracy of these algorithms is better than for the dataflow ones, because we make use of control flow information. Our algorithms also compare favorably in complexity, but the dataflow approach is probably cheaper in most practical settings. In addition, our schemes can give information even in the presence of dynamically allocated data structures.

[776]

Claude Pair, Michaneh Amirchahy, and Danièle Néel. Preuves de descriptions de traitements de textes par attributs. rapport de recherche 163, IRIA-Laboria, Rocquencourt, March 1976.

[777]

Claude Pair, Michaneh Amirchahy, and Danièle Néel. Correctness proofs of syntax-directed processing descriptions by attributes. Journal of Computer and System Sciences, 19(1):1-17, August 1979.