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.

Integrating software testing and run-time checking in an assertion verification framework

We have designed and implemented a framework that unifies unit testing and run-time verification (as well as static verification and static debugging). A key contribution of our approach is that a unified assertion language is used for all of these tasks. We first propose methods for compiling runtime checks for (parts of) assertions which cannot be verified at compile-time via program transformation. This transformation allows checking preconditions and postconditions, including conditional postconditions, properties at arbitrary program points, and certain computational properties. The implemented transformation includes several optimizations to reduce run-time overhead. We also propose a minimal addition to the assertion language which allows defining unit tests to be run in order to detect possible violations of the (partial) specifications expressed by the assertions. This language can express for example the input data for performing the unit tests or the number of times that the unit tests should be repeated. We have implemented the framework within the Ciao/CiaoPP system and effectively applied it to the verification of ISO-prolog compliance and to the detection of different types of bugs in the Ciao system source code. Several experimental results are presented that ¡Ilústrate different trade-offs among program size, running time, or levéis of verbosity of the messages shown to the user.

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.

A generic preprocessor for program validation and debugging

We present a generic preprocessor for combined static/dynamic validation and debugging of constraint logic programs. Passing programs through the preprocessor prior to execution allows detecting many bugs automatically. This is achieved by performing a repertoire of tests which range from simple syntactic checks to much more advanced checks based on static analysis of the program. Together with the program, the user may provide a series of assertions which trigger further automatic checking of the program. Such assertions are written using the assertion language presented in Chapter 2, which allows expressing a wide variety of properties. These properties extend beyond the predefined set which may be understandable by the available static analyzers and include properties defined by means of user programs. In addition to user-provided assertions, in each particular CLP system assertions may be available for predefined system predicates. Checking of both user-provided assertions and assertions for system predicates is attempted first at compile-time by comparing them with the results of static analysis. This may allow statically proving that the assertions hold (Le., they are validated) or that they are violated (and thus bugs detected). User-provided assertions (or parts of assertions) which cannot be statically proved ñor disproved are optionally translated into run-time tests. The implementation of the preprocessor is generic in that it can be easily customized to different CLP systems and dialects and in that it is designed to allow the integration of additional analyses in a simple way. We also report on two tools which are instances of the generic preprocessor: CiaoPP (for the Ciao Prolog system) and CHIPRE (for the CHIP CLP(FL>) system). The currently existing analyses include types, modes, non-failure, determinacy, and computational cost, and can treat modules separately, performing incremental analysis.

An overview of the ciao multiparadigm language and program development environment and its design philosophy

We describe some of the novel aspects and motivations behind the design and implementation of the Ciao multiparadigm programming system. An important aspect of Ciao is that it provides the programmer with a large number of useful features from different programming paradigms and styles, and that the use of each of these features can be turned on and off at will for each program module. Thus, a given module may be using e.g. higher order functions and constraints, while another module may be using objects, predicates, and concurrency. Furthermore, the language is designed to be extensible in a simple and modular way. Another important aspect of Ciao is its programming environment, which provides a powerful preprocessor (with an associated assertion language) capable of statically finding non-trivial bugs, verifying that programs comply with specifications, and performing many types of program optimizations. Such optimizations produce code that is highly competitive with other dynamic languages or, when the highest levéis of optimization are used, even that of static languages, all while retaining the interactive development environment of a dynamic language. The environment also includes a powerful auto-documenter. The paper provides an informal overview of the language and program development environment. It aims at illustrating the design philosophy rather than at being exhaustive, which would be impossible in the format of a paper, pointing instead to the existing literature on the system.

An overview of ciao and its design philosophy

We provide an overall description of the Ciao multiparadigm programming system emphasizing some of the novel aspects and motivations behind its design and implementation. An important aspect of Ciao is that, in addition to supporting logic programming (and, in particular, Prolog), it provides the programmer with a large number of useful features from different programming paradigms and styles and that the use of each of these features (including those of Prolog) can be turned on and off at will for each program module. Thus, a given module may be using, e.g., higher order functions and constraints, while another module may be using assignment, predicates, Prolog meta-programming, and concurrency. Furthermore, the language is designed to be extensible in a simple and modular way. Another important aspect of Ciao is its programming environment, which provides a powerful preprocessor (with an associated assertion language) capable of statically finding non-trivial bugs, verifying that programs comply with specifications, and performing many types of optimizations (including automatic parallelization). Such optimizations produce code that is highly competitive with other dynamic languages or, with the (experimental) optimizing compiler, even that of static languages, all while retaining the flexibility and interactive development of a dynamic language. This compilation architecture supports modularity and separate compilation throughout. The environment also includes a powerful autodocumenter and a unit testing framework, both closely integrated with the assertion system. The paper provides an informal overview of the language and program development environment. It aims at illustrating the design philosophy rather than at being exhaustive, which would be impossible in a single journal paper, pointing instead to previous Ciao literature.

A tutorial on program development and optimization using the Ciao preprocessor

We present in a tutorial fashion CiaoPP, the preprocessor of the Ciao multi-paradigm programming system, which implements 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, non-failure, and bounds on resource consumption (time or space cost).

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.

Selectivity of diacylhydrazine insecticides to the predatory bug Orius laevigatus: In vivo and modeling/docking experiments

BACKGROUND: Knowledge of pesticide selectivity to natural enemies is necessary for a successful implementation of biological and chemical control methods in integrated pest management (IPM) programs. Diacylhydrazine (DAH)-based ecdysone agonists also known as molting-accelerating compounds (MACs) are considered a selective group of insecticides, and their compatibility with predatory Heteroptera, which are used as biological control agents, is known. However, their molecular mode of action has not been explored in beneficial insects such as Orius laevigatus (Fieber) (Hemiptera: Anthocoridae). RESULTS: In this project in vivo toxicity assays demonstrated that the DAH-based RH-5849, tebufenozide and methoxyfenozide have no toxic effect against O. laevigatus. The ligand-binding domain (LBD) of the ecdysone receptor (EcR) of O. laevigatus was sequenced and a homology protein model was constructed which confirmed a cavity structure with 12 ?-helixes, harboring the natural insect molting hormone 20-hydroxyecdysone. However, docking studies showed that a steric clash occurred for the DAH-based insecticides due to a restricted extent of the ligand-binding cavity of the EcR of O. laevigatus. CONCLUSIONS: The insect toxicity assays demonstrated that MACs are selective for O. laevigatus. The modeling/docking experiments are indications that these pesticides do not bind with the LBD-EcR of O. laevigatus and support that they show no biological effects in the predatory bug. These data help in explaining the compatible use of MACs together with predatory bugs in IPM programs. Keywords: Orius laevigatus, selectivity, diacylhydrazine insecticides, ecdysone receptor, homology modelling, docking studies.

Integrating software testing and run-time checking in an assertion verification framework.

We have designed and implemented a framework that unifies unit testing and run-time verification (as well as static verification and static debugging). A key contribution of our approach is that a unified assertion language is used for all of these tasks. We first propose methods for compiling runtime checks for (parts of) assertions which cannot be verified at compile-time via program transformation. This transformation allows checking preconditions and postconditions, including conditional postconditions, properties at arbitrary program points, and certain computational properties. The implemented transformation includes several optimizations to reduce run-time overhead. We also propose a minimal addition to the assertion language which allows defining unit tests to be run in order to detect possible violations of the (partial) specifications expressed by the assertions. This language can express for example the input data for performing the unit tests or the number of times that the unit tests should be repeated. We have implemented the framework within the Ciao/CiaoPP system and effectively applied it to the verification of ISO-prolog compliance and to the detection of different types of bugs in the Ciao system source code. Several experimental results are presented that illustrate different trade-offs among program size, running time, or levels of verbosity of the messages shown to the user.

Compatibilidad de Orius laevigatus (Fieber) (Hemiptera: Anthocoridae) y Nesidiocoris tenuis (Reuter)(Hemiptera: Miridae), depredadores importantes en cultivos hortícolas protegidos, con nuevas barreras físicas selectivas y modernos plaguicidas

La nueva legislación en materia fitosanitaria se dirige hacia una Gestión Integrada de Plagas (GIP). Estos programas dan preferencia a aquellos métodos más respetuosos y sostenibles con el medio ambiente, siendo piezas claves en ellos el control biológico, el físico y otros de carácter no químico. Sin embargo, el uso de insecticidas selectivos es a veces necesario para el adecuado manejo de plagas en cultivos hortícolas. Por ello, el objetivo general de este estudio es aportar conocimientos para mejorar el control de plagas en cultivos hortícolas, mediante la integración de tres estrategias de lucha: biológica, física y química. Una parte de este trabajo ha consistido en el estudio de los posibles efectos que mallas tratadas con insecticida (bifentrin) pudieran provocar mediante diferentes ensayos de laboratorio, invernadero y campo, en los enemigos naturales Orius laevigatus (Fieber) (Hemiptera: Anthocoridae) (depredador de trips), Nesidiocoris tenuis (Reuter) (Hemiptera: Miridae) (depredador de mosca blanca y Tuta absoluta (Meirick) (Lepidoptera: Gelechiidae)), y otros agentes de biocontrol comúnmente usados en cultivos hortícolas protegidos. Este tipo de mallas se han empleado con éxito en entomología médica para controlar mosquitos vectores de la malaria, y actualmente se está trabajando en su desarrollo para uso agrícola como método de exclusión, y método directo de control de plagas. En los ensayos realizados en laboratorio, O. laevigatus y N. tenuis no fueron capaces de detectar la presencia de bifentrin en el ensayo de preferencia. Además, no se produjo mortalidad a corto plazo (72 horas) en ambos chinches depredadores. Por el contrario, se registró una elevada mortalidad cuando se expusieron por contacto a la malla tratada durante 72 horas en cajas de dimensiones reducidas (10 cm de diámetro X 3 cm de altura). En ensayos llevados a cabo bajo condiciones más reales de exposición, en un invernadero experimental con jaulas de 25 X 25 X 60 cm de altura, no se produjo ningún efecto en la mortalidad a corto plazo (72 horas) o en los parámetros reproductivos de O. laevigatus y N. tenuis. Finalmente, en ensayos de campo realizados en túneles semi-comerciales (8 m de largo X 6,5 m de ancho X 2,6 m de altura), ni las condiciones ambientales [temperatura, humedad relativa, radiación ultravioleta (UV) y fotosintéticamente activa (PAR)], ni los enemigos naturales, se vieron afectados por la presencia de la malla tratada con bifentrin en el cultivo. Sin embargo, los resultados no fueron concluyentes, debido al bajo establecimiento de los agentes de biocontrol liberados. Por lo tanto, más estudios son necesarios en invernaderos comerciales para confirmar los resultados preliminares de compatibilidad. Además, en este trabajo se han evaluado los efectos letales (mortalidad) y subletales (parámetros reproductivos) de seis modernos insecticidas sobre los chinches depredadores O. laevigatus y N. tenuis, mediante ensayos de laboratorio y persistencia. Los ensayos se realizaron por contacto residual, aplicando los insecticidas a la dosis máxima de campo sobre placas de cristal (laboratorio) o plantas (persistencia). Los productos fitosanitarios se seleccionaron por representar a un grupo de modernos plaguicidas con modos de acción en principio más selectivos para los enemigos naturales que antiguos plaguicidas como organoclorados, oroganofosforados o carbamatos, y por su uso frecuente en cultivos hortícolas donde O. laevigatus y N. tenuis están presentes. Todos ellos están incluidos o en proceso de inclusión en la lista comunitaria de sustancias activas para uso agrícola, Anexo I de la Directiva 91/414/CEE: abamectina y emamectina (avermectinas neurotóxicas, activadoras del canal del cloro), deltametrina (piretroide neurotóxico, modulador del canal del sodio, control positivo), flubendiamida (neurotóxico, modulador del receptor de rianodina), spinosad (naturalito neurotóxico, agonistas/antagonistas del receptor de nicotínico acetilcolina) y spiromesifen (inhibidor de la acetil CoA carboxilasa). El estudio mostró que O. laevigatus fue más susceptible a los insecticidas que N. tenuis. Además, los resultados revelaron que flubendiamida y spiromesifen fueron compatibles con los dos enemigos naturales estudiados, y por tanto se podrían usar en programas de GIP. Por el contrario, los insecticidas abamectina, deltametrina, emamectina y spinosad no fueron selectivos para ninguno de los chinches depredadores. Sin embargo, los estudios de persistencia demostraron que a pesar de que estos insecticidas no proporcionaron selectividad fisiológica, pueden proporcionar selectividad ecológica en algunos casos. Abamectina, deltametrina, emamectina y spinosad podrían ser compatibles con N. tenuis si el enemigo natural es introducido en el cultivo 4 días después de su aplicación. En el caso de O. laevigatus, abamectina, deltametrina y spinosad se clasificaron como persistentes, por lo tanto es necesario completar el estudio con experimentos de semi-campo y campo que determinen si es posible su uso conjunto en programas de GIP. Por otro lado, emamectina podría ser compatible con O. laevigatus si el enemigo natural es introducido en el cultivo 7 días después de su aplicación. Por último, se ha comprobado la selectividad de tres insecticidas aceleradores de la muda (MACs) (metoxifenocida, tebufenocida y RH-5849) sobre O. laevigatus y N. tenuis. Además de realizar estudios para evaluar la toxicidad en laboratorio de los insecticidas por contacto residual e ingestión (principal modo de acción de los MAC´s), se extrajo RNA de los insectos y con el cDNA obtenido se secuenció y clonó el dominio de unión al ligando (LBD) del receptor de ecdisona correspondiente a O. laevigatus (OlEcR-LBD) y N. tenuis (NtEcR-LBD). Posteriormente, se obtuvo la configuración en tres dimensiones del LBD y se estudió el acoplamiento de las moléculas de los tres insecticidas en la cavidad que forman las 12 α-hélices que constituyen el EcR-LBD. En el caso de N. tenuis se debe mencionar que no fue posible la obtención de la secuencia completa del LBD. Sin embargo, se obtuvo una secuencia parcial (hélice 6-hélice 11), que mostró una alta conservación de aminoácidos con respecto a la obtenida en O. laevigatus. Los ensayos de toxicidad mostraron que metoxifenocida, tebufenocida y RH-5849 no produjeron ningún efecto nocivo en ambos depredadores. Además, los estudios de modelado por homología y acoplamiento molecular llevados a cabo con O. laevigatus, también indicaron que los MACs no produjeron ningún efecto deletéreo en este enemigo natural. Por lo tanto, estos compuestos pueden ser aplicados de manera segura en programas de GIP en los cuales O. laevigatus y N. tenuis estén presentes. ABSTRACT The new pesticide legislation on pest control is aimed at integrated pest management (IPM). These programs are based on the most environmentally sustainable approaches, where biological, physical control and other non-chemical methods are the cornerstone. However, selective pesticides are often required for pest management on horticultural crops. Therefore, the main goal of this study is to provide knowledge to improve pest control on horticultural crops through the integration of three strategies: biological, physical and chemical. Firstly, the effects of insecticide treated nets (bifenthrin) were evaluated in different laboratory, greenhouse and field experiments on the natural enemies Orius laevigatus (Fieber) (Hemiptera: Anthocoridae) (predator of thrips), Nesidiocoris tenuis (Reuter) (Hemiptera: Miridae) (predator of whiteflies and Tuta absoluta (Meirick) (Lepidoptera: Gelechiidae)), and other biocontrol agents commonly used on protected horticultural crops. These types of nets have been successfully used in medical entomology to control mosquito malaria vectors, and work is currently being done on their use as exclusion barriers and as a direct method of pest control in agriculture. In experiments made under laboratory conditions, O. laevigatus and N. tenuis were not able to detect the presence of bifenthrin in a dual-choice test. Furthermore, no shortterm mortality (72 hours) was recorded on both predatory bugs. In contrast, a high mortality rate was found when they were exposed by contact to the bifenthrin-treated net for 72 hours in small cages (10 cm diameter X 3 cm high). In assays carried out under more realistic conditions of exposure, in an experimental greenhouse with cages of 25 X 25 X 60 cm high, short-term mortality (72 hours) and reproductive parameters were not affected. Lastly, in field experiments carried out in semi-commercial tunnels (8 m long X 6.5 m width X 2.6 m high), neither environmental conditions [temperature, relative humidity, ultraviolet (UV) and photosynthetically active radiation (PAR)] nor natural enemies were affected by the presence of the bifenthrin-treated net on the crop. However, results were not conclusive, mainly due to a low settlement of the released biocontrol agents, and further studies are needed in commercial greenhouses to confirm our preliminary results of compatibility. Secondly, the lethal (mortality) and sublethal effects (reproductive parameters) of six modern pesticides on the predatory bugs O. laevigatus and N. tenuis has been evaluated through laboratory and persistence experiments. Trials were carried out by residual contact, applying the insecticides to the maximum field recommended concentration on glass plates (laboratory) or plants (persistence). Insecticides were chosen as representatives of modern pesticides with a more selective mode of action on natural enemies than organochlorine, organophosphorus and carbamate insecticides. Moreover, they were also chosen because of their frequent use on horticultural crops where O. laevigatus and N. tenuis are present. All of them have been included or have been requested for inclusion in the community list of active substances on the agricultural market, Annex I of the European Directive 91/414/EEC: abamectin and emamectin (neurotoxic avermectins, chloride channel activators), deltamethrin (neutotoxic pyrethroid, sodium channel modulator, positive commercial standard), flubendiamide (neurotoxic, rianodine receptor modulator), spinosad (neurotoxic naturalyte, nicotinic acetylcholine receptor allosteric activator) and spiromesifen (inhibitors of acetyl CoA carboxylase). The study showed that O. laevigatus was more susceptible to all the studied pesticides than N. tenuis. In addition, the research results indicated no impact of flubendiamide and spiromesifen on the two natural enemies studied under laboratory conditions. Consequently, both pesticides are candidates to be included in IPM programmes where these biocontrol agents are present. On the other hand, abamectin, deltamethrin, emamectin and spinosad were not selective for both predatory bugs in laboratory experiments. However, persistence test demonstrated that in spite of the lack of physiological selectivity, these pesticides can provide ecological selectivity in some cases. Abamectin, deltamethrin, emamectin and spinosad could be compatible with N. tenuis if the mirid bug is released 4 days after the insecticide treatment on the crop. With regard to O. laevigatus, abamectin, deltamethrin and spinosad were classified as persistent in our assays, thus the study should be completed with semi-field and field experiments in order to ascertain their possible joint use in IPM programs. In contrast, emamectin could be compatible with O. laevigatus if the pirate bug is released 7 days after the insecticide treatment on the crop. Finally, the selectivity of three moulting accelerating compounds (MACs) (methoxyfenozide, tebufenozide and RH-5849) has also been evaluated on O. laevigatus and N. tenuis. In addition to laboratory experiments to evaluate the toxicity of the insecticides by residual contact and ingestion, molecular approaches were used as well. RNA of both insects was isolated, cDNA was subsequently synthesized and the complete sequence of the ligand binding domain (LBD) of the ecdysone receptor of O. laevigatus (OlEcR-LBD) and N. tenuis (NtEcR-LBD) were determined. Afterwards, the three dimensional structure of LBD was constructed. Finally, the docking of the insecticide molecules in the cavity delineated by the 12 α-helix that composed the EcRLBD was performed. In the case of N. tenuis, it should be noted that in spite of intensive efforts, we did not manage to complete the sequence for the LBD.However, a partial sequence of the LBD was obtained (helix 6-helix 11), and a strong conservation between the amino acids of N. tenuis and O. laevigatus was observed. Results showed no biological activity of methoxyfenozide, tebufenozide and RH-5849, on both predatory bugs. Moreover, modeling of the OlEcR-LBD and docking experiments also suggested that MACs were devoid of any deleterious effect on O. laevigatus. Therefore, our results indicate that these compounds could be safely applied in IPM programs in which O. laevigatus and N. tenuis are present.