{"content":[{"text":"Mechanical Veriﬁcation of Interactive Programs \n speciﬁed by Use Cases \n Guillaume Claret∗, Yann Régis-Gianas∗ \n ∗ Univ Paris Diderot, Sorbonne Paris Cité, \n PPS, UMR 7126 CNRS, \n PiR2, INRIA Paris-Rocquencourt, \n F-75205 Paris, France \n http://guillaume.claret.me/ and http://yann.regis-gianas.org/","bbox":{"left":0.123309,"top":0.064908,"width":0.753409,"height":0.18710600000000002}},{"text":"Abstract—Interactive programs, like user interfaces, \n are hard to formally specify and thus to prove cor- \n rect. Some ideas coming from functional programming \n languages have been successful to improve the way we \n write safer programs, compared to traditional imper- \n ative languages, but these ideas mostly apply to code \n fragments without any inputs–outputs. \n Using the purely functional language Coq, we present \n a new technique to represent interactive programs and \n formally verify use cases using the Coq proof engine \n as a symbolic debugger. To this end we introduce the \n notion of scenarios, well-typed schema of interactions \n between an environment and a program. We design and \n certify a blog system as an illustration. Our approach \n generalizes unit-testing techniques and outlines a new \n method for mechanically assisted checking of eﬀectful \n functional programs. \n I. Introduction \n Implementing and proving correct interactive programs \n is challenging. Indeed, interactive programs are hard to \n reason about because they communicate with an outer \n environment (the operating system, the network, the \n user, . . . ) which may be under-speciﬁed and non determin- \n istic. Moreover, the communications between the program \n and the environment can happen at many points during \n the execution and may depend on previous interactions. \n Many techniques have been developed to model, specify \n and prove correct interactive or concurrent programs[15]. \n For instance, process algebra and temporal logics are well \n understood abstract models for such programs. In these \n abstract models, some interesting behavioral properties \n can be automatically proved by model-checkers. Yet, these \n tools usually provide guarantees about the model of the \n program, not its actual implementation. \n In another approach, called software-proof co-design, \n the speciﬁcation and the veriﬁcation of a program is \n not disconnected from its actual implementation. In that \n case, specifying, implementing and verifying are tightly \n interleaved in the software development process. This \n tight integration is possible within the Coq proof assistant \n which is both a programming language and an assisted \n prover. Yet, even if a realistic compiler for the C language \n has already been developed in Coq[12], using Coq as a \n general purpose programming language may be considered","bbox":{"left":0.079998,"top":0.281621,"width":0.41046999999999995,"height":0.635525}},{"text":"a tour de force especially because it is purely functional \n and only accepts total and terminating functions. Our \n objective is to alleviate the cost of certiﬁed programming \n (i) by importing monadic programming technique from \n the Haskell programming language to express eﬀectful and \n partial computations ; (ii) by mechanizing mainstream \n software engineering techniques inside Coq to ease the \n migration from unveriﬁed to veriﬁed speciﬁcations. \n In software development processes, use cases[10] are \n commonly used to specify and verify programs with \n inputs–outputs. A use case is basically a list of interaction \n steps between a program and an environment, in order to \n denote functional properties. A use case can be veriﬁed \n by manually running the program or by automated unit- \n testing. However, unit-testing methods are never complete \n as soon as there is an inﬁnite set of possible values for the \n program inputs. We will show how to verify use cases on \n inﬁnitely many inputs using the notion of scenarios. \n A lot of ideas coming from functional programming \n languages changed the way we structure software today. \n Among these ideas are the use of composable higher-order \n functions as the main building block[9], referentially trans- \n parent expressions, algebraic data types, polymorphic[16] \n and dependent types[19]. Many programmers now use \n these ideas to increase the modularity and the correctness \n of their programs. \n One of the limitations of most functional programming \n approaches is that they are often only eﬀective on the \n pure (as \"without inputs and outputs\") fragments of a \n program. Other methodologies are required to write the \n impure (or interactive) parts (see for example [11]). For \n example, in the functional language Haskell, the impure \n computations are represented into a monad[23] using some \n special combinators. This monad isolates by typing the \n pure and impure computations, but oﬀers limited ways to \n reason about the correctness of the inputs–outputs. \n To extend and continue with the techniques developed \n in Haskell, we chose the purely functional language Coq \n to write and mechanically certify interactive programs. \n Coq is both a purely functional language and a theo- \n rem prover. The theory of Coq is based on the CIC[5] \n (the Calculus of Inductive Constructions type theory). It","bbox":{"left":0.50976,"top":0.28043,"width":0.41046800000000006,"height":0.636954}}],"images_bbox":[],"images_bbox_not_text_overlap":[]}