Programmation impérative | EPFL Graph Search

En informatique, la programmation impérative est un paradigme de programmation qui décrit les opérations en séquences d'instructions exécutées par l'ordinateur pour modifier l'état du programme. Ce type de programmation est le plus répandu parmi l'ensemble des langages de programmation existants, et se différencie de la programmation déclarative (dont la programmation logique ou encore la programmation fonctionnelle sont des sous-ensembles). Langages impératifs et processeurs La quasi-totalité des processeurs qui équipent les ordinateurs sont de nature impérative : ils sont faits pour exécuter une suite d'instructions élémentaires, codées sous forme d'opcodes (pour operation codes). L'ensemble des opcodes forme le langage machine spécifique à l'architecture du processeur. L'état du programme à un instant donné est défini par le contenu de la mémoire centrale à cet instant. Les langages de plus haut niveau utilisent des variables et des opérations plus complexes, mais suive

Database Queries in Java

Christopher Ming-Yee Iu

In conventional programming languages like Java, the interface for accessing databases is often inelegant. Typically, an entire separate database query language must be embedded inside a conventional programming language for programmers to access the full power and speed of a database. Programmers, though, prefer working entirely from within their conventional programming languages, both for general-purpose computation and for database access. This thesis explores how database operations can be expressed using the existing syntax of conventional programming languages. Programmers are able to write all their code –both general purpose code and database access code– in a single language. To run these database operations efficiently though, algorithms are needed for finding these database operations and optimizing them. This thesis focuses on techniques that can be easily adopted because they do not require changes to existing compilers. Three systems have been developed: Queryll, JReq, and HadoopToSQL. Each system examines the problem from the context of functional-style code, imperative-style code, and MapReduce-style code respectively.

EPFL2010

Scaling Language Features for Program Verification

Georg Stefan Schmid

Formal verification of real-world software systems remains challenging for a number of reasons, including lack of automation, friction in specifying properties, and limited support for the diverse programming paradigms used in industry. In this thesis we make progress towards a better verification experience in general-purpose programming languages by contributing improvements both to the automated checking and the specification of safety properties in languages combining functional and imperative features. We present our extensions in two parts -- reasoning about shared mutable data, and types as specifications -- both of which ultimately rely on reductions of expressive surface languages to a functional core. Throughout, we instantiate our techniques for the particular example of Scala, a mixed-paradigm language widely-used in industry.The first part shows how to extend a verifier for higher-order functions and immutable data to support imperative programs with shared mutable data. We build upon Stainless, a contract-based verification system that relies on SMT solvers to automatically verify a large fragment of Scala. Our technique extends Stainless to check general heap-manipulating programs against modular specifications in the style of dynamic frames. A novelty of our approach is the translation of imperative function contracts that encodes frame conditions using quantifier-free formulas in first-order logic, instead of relying on quantifiers or on dedicated separation logic reasoning. Our quantifier-free encoding enables SMT solvers to both prove safety and to report counterexamples relative to the semantics of procedure contracts.In the second part we turn to types and type-level programming as an alternative means of specifying correctness properties. While dependent types have been studied extensively for purely-functional languages, we investigate their applications to languages with subtyping and (abstractions of) imperative features. We first study a calculus that provides type-level computation through singleton types and allows abstraction of state and IO through a non-deterministic choice operator. This allows for modelling interactions with existing imprecisely-typed and impure code. Our calculus is formalized and mechanically proven correct using the Coq proof assistant. In addition, we develop a prototypical implementation in the Scala compiler and study typical type-level programming use cases in the Scala ecosystem.

EPFL2022

Scaling Language Features for Program Verification

Georg Stefan Schmid

EPFL2022