Mechanical Verification of Interactive Programs Specified by Use Cases

International audienceInteractive programs, like user interfaces, are hard to formally specify and thus to prove correct. Some ideas coming from functional programming languages have been successful to improve the way we write safer programs, compared to traditional imperative languages, but these ideas mostly apply to code fragments without any inputs–outputs. Using the purely functional language Coq, we present a new technique to represent interactive programs and formally verify use cases using the Coq proof engine as a symbolic debugger. To this end we introduce the notion of scenarios, well-typed schema of interactions between an environment and a program. We design and certify a blog system as an illustration. Our approach generalizes unit-testing techniques and outlines a new method for mechanically assisted checking of effectful functional programs. I. Introduction Implementing and proving correct interactive programs is challenging. Indeed, interactive programs are hard to reason about because they communicate with an outer environment (the operating system, the network, the user,. . .) which may be under-specified and non determin-istic. Moreover, the communications between the program and the environment can happen at many points during the execution and may depend on previous interactions. Many techniques have been developed to model, specify and prove correct interactive or concurrent programs[15]. For instance, process algebra and temporal logics are well understood abstract models for such programs. In these abstract models, some interesting behavioral properties can be automatically proved by model-checkers. Yet, these tools usually provide guarantees about the model of the program, not its actual implementation. In another approach, called software-proof co-design, the specification and the verification of a program is not disconnected from its actual implementation. In that case, specifying, implementing and verifying are tightly interleaved in the software development process. This tight integration is possible within the Coq proof assistant which is both a programming language and an assisted prover. Yet, even if a realistic compiler for the C language has already been developed in Coq[12], using Coq as a general purpose programming language may be considere