Refinement is a generic term of computer science that encompasses various approaches for producing correct computer programs and simplifying existing programs to enable their formal verification.
In formal methods, program refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete (low-level) executable program. Stepwise refinement allows this process to be done in stages. Logically, refinement normally involves implication, but there can be additional complications.
The progressive just-in-time preparation of the product backlog (requirements list) in agile software development approaches, such as Scrum, is also commonly described as refinement.
Data refinement is used to convert an abstract data model (in terms of sets for example) into implementable data structures (such as arrays). Operation refinement converts a specification of an operation on a system into an implementable program (e.g., a procedure). The postcondition can be strengthened and/or the precondition weakened in this process. This reduces any nondeterminism in the specification, typically to a completely deterministic implementation.
For example, x ∈ {1,2,3} (where x is the value of the variable x after an operation) could be refined to x ∈ {1,2}, then x ∈ {1}, and implemented as x := 1. Implementations of x := 2 and x := 3 would be equally acceptable in this case, using a different route for the refinement. However, we must be careful not to refine to x ∈ {} (equivalent to false) since this is unimplementable; it is impossible to select a member from the empty set.
The term reification is also sometimes used (coined by Cliff Jones). Retrenchment is an alternative technique when formal refinement is not possible. The opposite of refinement is abstraction.
Refinement calculus is a formal system (inspired from Hoare logic) that promotes program refinement. The FermaT Transformation System is an industrial-strength implementation of refinement.
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.
Un algorithme est correct s'il fait ce qu'on attend de lui. Plus précisément, rappelons qu'un algorithme est décrit par une spécification des données sur lesquelles l'algorithme va démarrer son calcul et une spécification du résultat produit par l'algorithme. Démontrer la correction de l'algorithme consiste à démontrer que l'algorithme retourne, quand il calcule en partant des données, un objet qui est un des résultats escomptés et qui satisfait la spécification du résultat comme énoncé dans la description de l'algorithme.
La programmation par contrat (en anglais, design by contract ou DBC) est un paradigme de programmation dans lequel le déroulement des traitements est régi par des règles. Ces règles, appelées des assertions, forment un contrat qui précise les responsabilités entre le client et le fournisseur d'un morceau de code logiciel. C'est une méthode de programmation semi-formelle dont le but principal est de réduire le nombre de bugs dans les programmes.
Se concentre sur l'utilisation d'Inox pour la vérification des programmes, en démontrant le processus de vérification des programmes et en assurant l'exactitude.
We introduce a two-level preconditioner for the efficient solution of large scale saddle point linear systems arising from the finite element (FE) discretization of parametrized Stokes equations. This preconditioner extends the Multi Space Reduced Basis (M ...
Statically typed languages verify programs at compile-time. As a result many programming mistakes are detected at an early stage of development. A programmer does not have to specify types for every single term manually, however. Many programming languages ...
[Context] With the expansion of services and service science, service systems have become an important abstraction for the service revolution. Service is defined as the application of resources (including competences, skills, and knowledge) to make changes ...