Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging

We discuss a framework for the application of abstract interpretation as an aid during program development, rather than in the more traditional application of program optimization. Program validation and detection of errors is first performed statically by comparing (partial) specifications written in terms of assertions against information obtained from (global) static analysis of the program. The results of this process are expressed in the user assertion language. Assertions (or parts of assertions) which cannot be checked statically are translated into run-time tests. The framework allows the use of assertions to be optional. It also allows using very general properties in assertions, beyond the predefined set understandable by the static analyzer and including properties defined by user programs. We also report briefly on an implementation of the framework. The resulting tool generates and checks assertions for Prolog, CLP(R), and CHIP/CLP(fd) programs, and integrates compile-time and run-time checking in a uniform way. The tool allows using properties such as types, modes, non-failure, determinacy, and computational cost, and can treat modules separately, performing incremental analysis.

Using global analysis, partial specifications, and an extensible assertion language for program validation and debugging

We present a framework for the application of abstract interpretation as an aid during program development, rather than in the more traditional application of program optimization. Program validation and detection of errors is first performed statically by comparing (partial) specifications written in terms of assertions against information obtained from static analysis of the program. The results of this process are expressed in the user assertion language. Assertions (or parts of assertions) which cannot be verified statically are translated into run-time tests. The framework allows the use of assertions to be optional. It also allows using very general properties in assertions, beyond the predefined set understandable by the static analyzer and including properties defined by means of user programs. We also report briefly on an implementation of the framework. The resulting tool generates and checks assertions for Prolog, CLP(R), and CHIP/CLP(fd) programs, and integrates compile-time and run-time checking in a uniform way. The tool allows using properties such as types, modes, non-failure, determinacy, and computational cost, and can treat modules separately, performing incremental analysis. In practice, this modularity allows detecting statically bugs in user programs even if they do not contain any assertions.

Analysing written production competence descriptors for academic and professional purposes and their calibration to the CEFR

The Common European Framework of Reference for Languages (CEFR) "describes in a comprehensive way what language learners have to learn to do in order to use a language for communication and what knowledge and skills they have to develop so as to be able to act effectively" (Council of Europe, 2001: 1). This paper reports on the findings of two studies whose purpose was to assess written production competence descriptors meant for their inclusion into the Academic and Professional English Language Portfolio KELP) for students of engineering and architecture. The main objective of these studies was to establish whether the language competence descriptors were a satisfactory valid tool in their language programmes from the point of view of clarity, relevance and reliability, as perceived by the students and fellow English for Academic Purposes (RAP) / English for Science and Technology (EST) instructors. The studies shed light on how to improve unsatisfactory descriptors. Results show that the final descriptor lists were on the whole well calibrated and fairly well written: the great majority was considered valid for both teachers and students involved.