Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor)

The technique of Abstract Interpretation has allowed the development of very sophisticated global program analyses which are at the same time provably correct and practical. We present in a tutorial fashion a novel program development framework which uses abstract interpretation as a fundamental tool. The framework uses modular, incremental abstract interpretation to obtain information about the program. This information is used to validate programs, to detect bugs with respect to partial specifications written using assertions (in the program itself and/or in system libraries), to generate and simplify run-time tests, and to perform high-level program transformations such as multiple abstract specialization, parallelization, and resource usage control, all in a provably correct way. In the case of validation and debugging, the assertions can refer to a variety of program points such as procedure entry, procedure exit, points within procedures, or global computations. The system can reason with much richer information than, for example, traditional types. This includes data structure shape (including pointer sharing), bounds on data structure sizes, and other operational variable instantiation properties, as well as procedure-level properties such as determinacy, termination, nonfailure, and bounds on resource consumption (time or space cost). CiaoPP, the preprocessor of the Ciao multi-paradigm programming system, which implements the described functionality, will be used to illustrate the fundamental ideas.

Program development using abstract interpretation (and the ciao system preprocessor)

The technique of Abstract Interpretation has allowed the development of very sophisticated global program analyses which are at the same time provably correct and practical. We present in a tutorial fashion a novel program development framework which uses abstract interpretation as a fundamental tool. The framework uses modular, incremental abstract interpretation to obtain information about the program. This information is used to validate programs, to detect bugs with respect to partial specifications written using assertions (in the program itself and/or in system librarles), to genérate and simplify run-time tests, and to perform high-level program transformations such as múltiple abstract specialization, parallelization, and resource usage control, all in a provably correct way. In the case of validation and debugging, the assertions can refer to a variety of program points such as procedure entry, procedure exit, points within procedures, or global computations. The system can reason with much richer information than, for example, traditional types. This includes data structure shape (including pointer sharing), bounds on data structure sizes, and other operational variable instantiation properties, as well as procedure-level properties such as determinacy, termination, non-failure, and bounds on resource consumption (time or space cost). CiaoPP, the preprocessor of the Ciao multi-paradigm programming system, which implements the described functionality, will be used to illustrate the fundamental ideas.

Detection of Wuchereria bancrofti DNA in paired serum and urine samples using polymerase chain reaction-based systems

The Global Program for the Elimination of Lymphatic Filariasis (GPELF) aims to eliminate this disease by the year 2020. However, the development of more specific and sensitive tests is important for the success of the GPELF. The present study aimed to standardise polymerase chain reaction (PCR)-based systems for the diagnosis of filariasis in serum and urine. Twenty paired biological urine and serum samples from individuals already known to be positive for Wuchereria bancrofti were collected during the day. Conventional PCR and semi-nested PCR assays were optimised. The detection limit of the technique for purified W. bancrofti DNA extracted from adult worms was 10 fg for the internal systems (WbF/Wb2) and 0.1 fg by using semi-nested PCR. The specificity of the primers was confirmed experimentally by amplification of 1 ng of purified genomic DNA from other species of parasites. Evaluation of the paired urine and serum samples by the semi-nested PCR technique indicated only two of the 20 tested individuals were positive, whereas the simple internal PCR system (WbF/Wb2), which has highly promising performance, revealed that all the patients were positive using both samples. This study successfully demonstrated the possibility of using the PCR technique on urine for the diagnosis of W. bancrofti infection.

Etude systématique, cladistique et biogéographique des Baetidae (Ephemeroptera) de Madagascar

Les Ephéméroptères constituent un ordre très archaïque d?insectes ailés, comprenant un nombre réduit d?espèces (actuellement environ 2500 espèces). Les larves sont aquatiques; la durée de ce stade est en général d?une année. Le stade adulte est par contre extrêmement bref: de quelques heures à quelques jours. La fonction quasi unique de ce stade est la reproduction. Par sa superficie, Madagascar est la quatrième île du monde. Elle est située dans la partie occidentale de l?Océan Indien à plus de 300 km de la côte africaine. Madagascar faisait partie du super-continent Gondwana. Elle s?est séparée de l?Afrique (-165 M.a.), puis a migré vers le Sud (-125 M.a.) avant de se détacher du sous-continent indien (-65 M.a.). La connaissance des Ephéméroptères malgaches était, jusqu?à très récemment, extrêmement limitée. Grâce au programme Biodiversité et biotypologie des eaux continentales malgaches, lancé conjointement par l?ORSTOM (actuel IRD, France) et le CNRE (Madagascar), un inventaire à large échelle de la macrofaune benthique malgache a été entrepris. La systématique de plusieurs familles d?Ephéméroptères (Tricorythidae, Polymitarcyidae, Palingeniidae,?), ainsi que d?autres groupes d?invertébrés (Trichoptères, Simuliidae, macrocrustacés) a fait l?objet d?études approfondies. La présente étude consistue un des volets de ce programme. Jusqu?au milieu des années 1990, seules quatre espèces valides appartenant à trois genres différents étaient décrites de Madagascar. En 6 ans, ce ne sont pas moins de 25 articles qui sont consacrés à la systématique des Baetidae, permettant de décrire 50 espèces et 8 genres nouveaux. La faune malgache des Baetidae compte actuellement 22 genres et 54 espèces. Malgré sa taille, Madagascar possède une richesse, tant générique que spécifique équivalente à celle d?un continent. Notre connaissance des Baetidae est suffisamment avancée pour mener une étude cladistique et biogéographique. La reconstruction phylogénétique a permis de mettre en évidence cinq lignées principales à Madagascar et de préciser, pour chacune d?elles, les genres inclus et les caractères propres. La faune des Baetidae malgaches présente un taux d?endémicité très élevé: 53 des 54 espèces et un tiers des genres sont endémiques. Elle montre des affinités extrêmement fortes avec la faune africaine, puisque 90% des genres présents à Madagascar ou en Afrique ont une répartition strictement restreinte à cette région. Les autres composantes, notamment orientales et océaniennes, sont négligeables; ces régions n?ont en commun avec Madagascar qu?un nombre restreint de genres cosmopolites. Ces affinités sont en contradiction avec les données géologiques de la dislocation du Gondwana. Plusieurs explications peuvent être données pour résoudre cette contradiction. La plus vraisemblable est que le pouvoir de dispersion des Ephéméroptères, et des Baetidae en particulier, est nettement sous-estimé. L?étude des faunes des îles volcaniques récentes, telles que les Comores, démontre clairement que les Baetidae sont capables de dispersion sur une distance de plus de 300 km. Il est donc possible d?envisager une colonisation de Madagascar à partir de l?Afrique continentale postérieure à la séparation des deux plaques. Nous avons établi des scénarios retraçant l?histoire biogéographique de chacune des cinq lignées. Pour quatre d?entre elles, l?Afrique continentale est le centre d?origine. La cinquième lignée aurait une origine paléarctique; l?Afrique représenterait un centre secondaire de spéciation. Ces lignées auraient secondairement colonisé Madagascar à partir de l?Afrique continentale. Ce travail ouvre donc d?importantes perspectives. Il rend possible l?utilisation à un niveau générique, voire spécifique, des Baetidae pour des travaux de faunistique ou d?écologie, en particulier pour des études liées à la dégradation de la qualité de l?eau. Il devrait également pouvoir servir de base pour l?étude et la compréhension des phénomènes de dispersion et colonisation dans les îles et archipels de l?Ouest de l?Océan Indien.<br/><br/>Mayflies (Ephemeroptera) are among the oldest known flying insects and encompass a very small number of species (ca 2500 species). Larvae are strictly freshwater inhabitants; this stage lasts generally one year. The imaginal stage is extremely short, from few hours to few days, and is devoted almost entirely to reproduction. Madagascar is the fourth largest island in the world by area. It is situated in the western part of the Indian Ocean, at a distance of more than 300 km from the African coast. Madagascar belonged to Gondwana. It was first separated from the African plate (-165 M.y.), then moved to the South (-65 M.y.), before the break-off with the Indian plate (-65 M.y.). Knowledge of the Malagasy mayflies was until recently extremely poor. The program Biodiversity and Biotypology of Malagasy Freshwaters, jointly run by the French ORSTOM and the Malagasy CNRE, began a global survey of the freshwater macroinvertebrates. The systematics of several mayfly families (Tricorythidae, Polymitarcyidae, Palingeniidae,?), and other invertebrate groups (Caddisflies, Blackflies,?) was the subject of ground studies. Our present study is one part of this global program. Until the middle of the nineties, only four baetid species belonging to three different genera had been described from Madagascar. During the last six years, 25 papers were dedicated to the systematics of the Baetidae, allowing the description of 50 new species and 8 new genera. The Malagasy fauna encompasses now 22 genera and 54 species. Despite its size, Madagascar has the same diversity, at specific and generic level, as a continent. Our knowledge of the Baetidae is sufficient to perform a cladistic and biogeographical study. Our phylogenetic reconstruction allows us to propose five main lineages and to indicate, for each of them, the genera included and their features. The Malagasy fauna of Baetidae possesses a high level of endemicity: 53 of the 54 species and one third of the genera are endemic. It shows extremely strong affinities with the African fauna, as more than 90% of the genera present in Madagascar or in Africa have a distribution restricted to this area. Other components, especially Oriental and Oceanian, are negligible. These areas share with Madagascar only a few widespread genera. These African affinities are in contradiction with the geological events, especially the break-off history of Gondwana. Some explanations can be given to solve this contradiction. The most likely is that the dispersal power of the mayflies, especially of the Baetidae, is greatly underestimated. The study of recent volcanic islands, particularly of the Comoros, clearly demonstrates that the Baetidae are able to disperse over more than 300 km. Consequently, a colonisation by the Baetidae, of Madagascar from the continental Africa, after the break-off must be considered as possible. We have established scenarios explaining the biogeographical history of each of the five lineages. For four of them, Africa has to be regarded as the centre of origin. The fifth lineage probably has a Palearctic origin; Africa should be considered as a secondary centre of speciation. These lineages should have secondarily colonised Madagascar from continental Africa. This work opens up new perspectives. It allows the use of the Baetidae for faunistic and ecological studies, especially for problems related to water quality. It must be also considered as a first step for understanding the dispersion and colonisation of the islands of the western part of the Indian Ocean.

Triple Structural Transition below Room Temperature in the Antifilarial Drug Diethylcarbamazine Citrate

A very unusual triple structural transition pattern below room temperature was observed for the antifilarial drug diethylcarbamazine citrate. Besides the first thermal, crystallographic, and vibrational investigations of this first-line drug used in clinical treatment for lymphatic filariasis, a noteworthy behavior with three structural transformations as a function of temperature was demonstrated by differential scanning calorimetry, Raman spectroscopy, and single-crystal X-ray diffractometry. Our X-ray data on single crystals allow for a complete featuring and understanding of all transitions, since the four structures associated with the three solid-solid phase transformations were accurately determined. Two of three structural transitions show an order-disorder mechanism and temperature hysteresis with exothermic peaks at 224 K (T(1)`) and 213 K (T(2)`) upon cooling and endothermic ones at 248 K (T(1)) and 226 K (T(2)) upon heating. The other transition occurs at 108 K (T(3)) and it is temperature-rate sensitive. Molecular displacements onto the (010) plane and conformational changes of the diethylcarbamazine backbone as a consequence of the C-H center dot center dot center dot N hydrogen bonding formation/cleavage between drug molecules explain the mechanism of the transitions at T(1)`/T(2). However, such changes are observed only on alternate columns of the drug intercalated by citrate chains, which leads to a doubling of the lattice period along the a axis of the 235 K structure with respect to the 150 and 293 K structures. At T(2)`/T(1), these structural alterations occur in all columns of the drug. At T(3), there is a rotation on the axis of the N-C bond between the carbamoyl moiety and an ethyl group of one crystallographically independent diethylcarbamazine molecule besides molecular shifts and other conformational alterations. The impact of this study is based on the fascinating finding in which the versatile capability of structural adaptation dependent on the thermal history was observed for a relatively simple organic salt, diethylcarbamazine citrate.

A model for inter-module analysis and optimizing compilation

Recent research into the implementation of logic programming languages has demonstrated that global program analysis can be used to speed up execution by an order of magnitude. However, currently such global program analysis requires the program to be analysed as a whole: sepárate compilation of modules is not supported. We describe and empirically evalúate a simple model for extending global program analysis to support sepárate compilation of modules. Importantly, our model supports context-sensitive program analysis and multi-variant specialization of procedures in the modules.

The ciao prolog system

Ciao is a public domain, next generation multi-paradigm programming environment with a unique set of features: Ciao offers a complete Prolog system, supporting ISO-Prolog, but its novel modular design allows both restricting and extending the language. As a result, it allows working with fully declarative subsets of Prolog and also to extend these subsets (or ISO-Prolog) both syntactically and semantically. Most importantly, these restrictions and extensions can be activated separately on each program module so that several extensions can coexist in the same application for different modules. Ciao also supports (through such extensions) programming with functions, higher-order (with predicate abstractions), constraints, and objects, as well as feature terms (records), persistence, several control rules (breadth-first search, iterative deepening, ...), concurrency (threads/engines), a good base for distributed execution (agents), and parallel execution. Libraries also support WWW programming, sockets, external interfaces (C, Java, TclTk, relational databases, etc.), etc. Ciao offers support for programming in the large with a robust module/object system, module-based separate/incremental compilation (automatically -no need for makefiles), an assertion language for declaring (optional) program properties (including types and modes, but also determinacy, non-failure, cost, etc.), automatic static inference and static/dynamic checking of such assertions, etc. Ciao also offers support for programming in the small producing small executables (including only those builtins used by the program) and support for writing scripts in Prolog. The Ciao programming environment includes a classical top-level and a rich emacs interface with an embeddable source-level debugger and a number of execution visualization tools. The Ciao compiler (which can be run outside the top level shell) generates several forms of architecture-independent and stand-alone executables, which run with speed, efficiency and executable size which are very competive with other commercial and academic Prolog/CLP systems. Library modules can be compiled into compact bytecode or C source files, and linked statically, dynamically, or autoloaded. The novel modular design of Ciao enables, in addition to modular program development, effective global program analysis and static debugging and optimization via source to source program transformation. These tasks are performed by the Ciao preprocessor ( ciaopp, distributed separately). The Ciao programming environment also includes lpdoc, an automatic documentation generator for LP/CLP programs. It processes Prolog files adorned with (Ciao) assertions and machine-readable comments and generates manuals in many formats including postscript, pdf, texinfo, info, HTML, man, etc. , as well as on-line help, ascii README files, entries for indices of manuals (info, WWW, ...), and maintains WWW distribution sites.

A fenntartható fejlődéssel foglalkozó nemzetközi együttműködés négy évtizede (Four Decades of International Cooperation on Sustainable Development)

Along with the recognition of the increasing environmental and social problems stemming from globalization, the need to address these problems and to develop the relevant international framework has strengthened since the 1970s. The scope of this cooperation gradually broadened and eventually it embraced all issues, which were considered to be critical for sustainable development. The summits on sustainability, namely, the UN Conference on Environment and Development in 1992, the “Rio+5” in 1997 and the World Summit on Sustainable Development in 2002, wished to respond to all unsustainable processes by adopting, reinforcing and expanding a global program. This program is based on a series of important principles and includes various goals and instruments adopted by consensus; however, it also reflects delicate compromises between development related aspirations and environmental barriers, and also between the developed and the developing countries. Actually, there is a serious implementation gap and there are also new challenges. Referring to these problems, the idea of convening an extraordinary summit in 2012 was raised and it was eventually adopted but with a rather narrow mandate and agenda. It turned out that besides the “usual” conflicts between the developed and developing countries e.g. upon the common but differentiated responsibilities or international development financing, there were also diverting views on the green economy and on the ways of institutional strengthening of the international sustainable development and environmental governance. As a consequence, the 2012 Conference concluded with rather modest results.

Geographic variation in the frequency of isolation and fluconazole and voriconazole susceptibilities of Candida glabrata: an assessment from the ARTEMIS DISK Global Antifungal Surveillance Program.

Geographic differences in frequency and azole resistance among Candida glabrata may impact empiric antifungal therapy choice. We examined geographic variation in isolation and azole susceptibility of C. glabrata. We examined 23 305 clinical isolates of C. glabrata during ARTEMIS DISK global surveillance. Susceptibility testing to fluconazole and voriconazole was assessed by disk diffusion, and the results were grouped by geographic location: North America (NA) (2470 isolates), Latin America (LA) (2039), Europe (EU) (12 439), Africa and the Middle East (AME) (728), and Asia-Pacific (AP) (5629). Overall, C. glabrata accounted for 11.6% of 201 653 isolates of Candida and varied as a proportion of all Candida isolated from 7.4% in LA to 21.1% in NA. Decreased susceptibility (S) to fluconazole was observed in all geographic regions and ranged from 62.8% in AME to 76.7% in LA. Variation in fluconazole susceptibility was observed within each region: AP (range, 50-100% S), AME (48-86.9%), EU (44.8-88%), LA (43-92%), and NA (74.5-91.6%). Voriconazole was more active than fluconazole (range, 82.3-84.2% S) with similar regional variation. Among 22 sentinel sites participating in ARTEMIS from 2001 through 2007 (84 140 total isolates, 8163 C. glabrata), the frequency of C. glabrata isolation increased in 14 sites and the frequency of fluconazole resistance (R) increased in 11 sites over the 7-year period of study. The sites with the highest cumulative rates of fluconazole R were in Poland (22% R), the Czech Republic (27% R), Venezuela (27% R), and Greece (33% R). C. glabrata was most often isolated from blood, normally sterile body fluids and urine. There is substantial geographic and institutional variation in both frequency of isolation and azole resistance among C. glabrata. Prompt species identification and fluconazole susceptibility testing are necessary to optimize therapy for invasive candidiasis.

Clinical outcome of patients with and without diabetes mellitus after percutaneous coronary intervention with the resolute zotarolimus-eluting stent: 2-year results from the prospectively pooled analysis of the international global RESOLUTE program

OBJECTIVES The aim of this study was to describe the process to obtain Food and Drug Administration (FDA) approval for the expanded indication for treatment with the Resolute zotarolimus-eluting stent (R-ZES) (Medtronic, Inc., Santa Rosa, California) in patients with coronary artery disease and diabetes. BACKGROUND The R-ZES is the first drug-eluting stent specifically indicated in the United States for percutaneous coronary intervention in patients with diabetes. METHODS We pooled patient-level data for 5,130 patients from the RESOLUTE Global Clinical Program. A performance goal prospectively determined in conjunction with the FDA was established as a rate of target vessel failure at 12 months of 14.5%. In addition to the FDA pre-specified cohort of less complex patients with diabetes (n = 878), we evaluated outcomes of the R-ZES in all 1,535 patients with diabetes compared with all 3,595 patients without diabetes at 2 years. RESULTS The 12-month rate of target vessel failure in the pre-specified diabetic cohort was 7.8% (upper 95% confidence interval: 9.51%), significantly lower than the performance goal of 14.5% (p < 0.001). After 2 years, the cumulative incidence of target lesion failure in patients with noninsulin-treated diabetes was comparable to that of patients without diabetes (8.0% vs. 7.1%). The higher risk insulin-treated population demonstrated a significantly higher target lesion failure rate (13.7%). In the whole population, including complex patients, rates of stent thrombosis were not significantly different between patients with and without diabetes (1.2% vs. 0.8%). CONCLUSIONS The R-ZES is safe and effective in patients with diabetes. Long-term clinical data of patients with noninsulin-treated diabetes are equivalent to patients without diabetes. Patients with insulin-treated diabetes remain a higher risk subset. (The Medtronic RESOLUTE Clinical Trial; NCT00248079; Randomized, Two-arm, Non-inferiority Study Comparing Endeavor-Resolute Stent With Abbot Xience-V Stent [RESOLUTE-AC]; NCT00617084; The Medtronic RESOLUTE US Clinical Trial (R-US); NCT00726453; RESOLUTE International Registry: Evaluation of the Resolute Zotarolimus-Eluting Stent System in a 'Real-World' Patient Population [R-Int]; NCT00752128; RESOLUTE Japan-The Clinical Evaluation of the MDT-4107 Drug-Eluting Coronary Stent [RJ]; NCT00927940).

Impact of overlapping newer generation drug-eluting stents on clinical and angiographic outcomes: pooled analysis of five trials from the international Global RESOLUTE Program

BACKGROUND Overlapping first generation sirolimus- and paclitaxel-eluting stents are associated with persistent inflammation, fibrin deposition and delayed endothelialisation in preclinical models, and adverse angiographic and clinical outcomes--including death and myocardial infarction (MI)--in clinical studies. OBJECTIVES To establish as to whether there are any safety concerns with newer generation drug-eluting stents (DES). DESIGN Propensity score adjustment of baseline anatomical and clinical characteristics were used to compare clinical outcomes (Kaplan-Meier estimates) between patients implanted with overlapping DES (Resolute zotarolimus-eluting stent (R-ZES) or R-ZES/other DES) against no overlapping DES. Additionally, angiographic outcomes for overlapping R-ZES and everolimus-eluting stents were evaluated in the randomised RESOLUTE All-Comers Trial. SETTING Patient level data from five controlled studies of the RESOLUTE Global Clinical Program evaluating the R-ZES were pooled. Enrollment criteria were generally unrestrictive. PATIENTS 5130 patients. MAIN OUTCOME MEASURES 2-year clinical outcomes and 13-month angiographic outcomes. RESULTS 644 of 5130 patients (12.6%) in the RESOLUTE Global Clinical Program underwent overlapping DES implantation. Implantation of overlapping DES was associated with an increased frequency of MI and more complex/calcified lesion types at baseline. Adjusted in-hospital, 30-day and 2-year clinical outcomes indicated comparable cardiac death (2-year overlap vs non-overlap: 3.0% vs 2.1%, p=0.36), major adverse cardiac events (13.3% vs 10.7%, p=0.19), target-vessel MI (3.9% vs 3.4%, p=0.40), clinically driven target vessel revascularisation (7.7% vs 6.5%, p=0.32), and definite/probable stent thrombosis (1.4% vs 0.9%, p=0.28). 13-month adjusted angiographic outcomes were comparable between overlapping and non-overlapping DES. CONCLUSIONS Overlapping newer generation DES are safe and effective, with comparable angiographic and clinical outcomes--including repeat revascularisation--to non-overlapping DES.

Impact of body mass index on long-term clinical outcomes after second-generation drug eluting stent implantation: Insights from the international global RESOLUTE program

BACKGROUND An increased body mass index (BMI) is associated with a high risk of cardiovascular disease and reduction in life expectancy. However, several studies reported improved clinical outcomes in obese patients treated for cardiovascular diseases. The aim of the present study is to investigate the impact of BMI on long-term clinical outcomes after implantation of zotarolimus eluting stents. METHODS Individual patient data were pooled from the RESOLUTE Clinical Program comprising five trials worldwide. The study population was sorted according to BMI tertiles and clinical outcomes were evaluated at 2-year follow-up. RESULTS Data from a total of 5,127 patients receiving the R-ZES were included in the present study. BMI tertiles were as follow: I tertile (≤ 25.95 kg/m(2) -Low or normal weight) 1,727 patients; II tertile (>25.95 ≤ 29.74 kg/m(2) -overweight) 1,695 patients, and III tertile (>29.74 kg/m(2) -obese) 1,705 patients. At 2-years follow-up no difference was found for patients with high BMI (III tertile) compared with patients with normal or low BMI (I tertile) in terms of target lesion failure (I-III tertile, HR [95% CI] = 0.89 [0.69, 1.14], P = 0.341; major adverse cardiac events (I-III tertile, HR [95% CI] = 0.90 [0.72, 1.14], P = 0.389; cardiac death (I-III tertile, HR [95% CI] = 1.20 [0.73, 1.99], P = 0.476); myocardial infarction (I-III tertile, HR [95% CI] = 0.86 [0.55, 1.35], P = 0.509; clinically-driven target lesion revascularization (I-III tertile, HR [95% CI] = 0.75 [0.53, 1.08], P = 0.123; definite or probable stent thrombosis (I-III tertile, HR [95% CI] = 0.98 [0.49, 1.99], P = 0.964. CONCLUSIONS In the present study, the patients' body mass index was found to have no impact on long-term clinical outcomes after coronary artery interventions.

Effectiveness of global analysis in strict independence-based automatic program parallelization

This paper presents a study of the effectiveness of global analysis in the parallelization of logic programs using strict independence. A number of well-known approximation domains are selected and tlieir usefulness for the application in hand is explained. Also, methods for using the information provided by such domains to improve parallelization are proposed. Local and global analyses are built using these domains and such analyses are embedded in a complete parallelizing compiler. Then, the performance of the domains (and the system in general) is assessed for this application through a number of experiments. We argüe that the results offer significant insight into the characteristics of these domains, the demands of the application, and the tradeoffs involved.

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.