Séance de cours

Test basé sur la propriété: QuickChick

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Description

Cette séance de cours de l'instructeur aborde le sujet des tests de propriété à l'aide de l'outil QuickChick. Il s'inscrit dans les concepts de test et de vérification, en mettant l'accent sur l'exactitude des logiciels à l'échelle par le biais de tests et de vérification. La séance de cours traite de l'importance des spécifications, du flou sur les propriétés et d'une étude de cas sur la non-ingérence. Il explore également le contrôle dynamique du flux d'information, l'exactitude de la sécurité de la mémoire spatiale pour C, et les défis rencontrés dans les tests pratiques basés sur des propriétés pour Python. L'instructeur présente le développement et l'application de QuickChick, un outil de test basé sur la propriété pour Coq, mettant en évidence ses réussites et l'intégration de la vérification formelle. La séance de cours se termine par des idées sur la façon de repousser les limites des essais sur la propriété et les orientations futures dans ce domaine.

Source officielle

Proximité ontologique

Génie informatique

Développement de logiciel: Software development process

Concepts associés (32)

Test (informatique)

vignette|Une programmeuse écrivant du code Java avec JUnit. En informatique, un test désigne une procédure de vérification partielle d'un système. Son objectif principal est d'identifier un nombre maximal de comportements problématiques du logiciel. Il permet ainsi, dès lors que les problèmes identifiés seront corrigés, d'en augmenter la qualité. D'une manière plus générale, le test désigne toutes les activités qui consistent à rechercher des informations quant à la qualité du système afin de permettre la prise de décisions.

Formal specification

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.

Software verification

Software verification is a discipline of software engineering, programming languages, and theory of computation whose goal is to assure that software satisfies the expected requirements. A broad definition of verification makes it related to software testing. In that case, there are two fundamental approaches to verification: Dynamic verification, also known as experimentation, dynamic testing or, simply testing. - This is good for finding faults (software bugs).

Software verification and validation

In software project management, software testing, and software engineering, verification and validation (V&V) is the process of checking that a software system meets specifications and requirements so that it fulfills its intended purpose. It may also be referred to as software quality control. It is normally the responsibility of software testers as part of the software development lifecycle.

Model-based testing

vignette|Diagramme du model-based testing Le model-based testing (MBT) est une activité qui permet de concevoir et de dériver (de manière automatique ou non) des cas de tests à partir d'un modèle abstrait et haut niveau du système sous test (SUT). Le modèle est dit abstrait car il offre bien souvent une vue partielle et discrète des comportements attendus d'un logiciel ou d'un système. Sur la base de modèles abstraits, des cas de test peuvent être dérivées sous la forme de suites de tests.

Afficher plus

Séances de cours associées (64)

Qu’est-ce que la vérification formelle?

Introduit la vérification formelle et ses avantages par rapport aux méthodes de test traditionnelles, en discutant de la démonstration automatique des théorèmes et en compilant les déclarations d'exactitude dans des conditions de vérification.

Correspondance logicielle: Test et vérification

Explore l'exactitude des logiciels grâce à des tests, à la vérification, au flou de propriété et au contrôle dynamique du flux d'information.

Introduction à la vérification formelle

Introduit la vérification formelle, en mettant l'accent sur la preuve rigoureuse de l'exactitude du système et l'utilisation de modèles mathématiques.

Des tests à la preuve

Explore les concepts d'ingénierie logicielle, en soulignant l'importance des tests et des spécifications claires pour assurer l'exactitude du logiciel.

Fusionner Trier: Tri Algorithme

Explique l'algorithme de tri de fusion, son exactitude et sa complexité temporelle par rapport à d'autres algorithmes de tri.

Afficher plus

Concepts associés (32)

Test (informatique)

Formal specification

Software verification

Software verification and validation

Model-based testing

Afficher plus