Iniciar sesiónCerrar
Correo:
Contraseña:
Entrar
Recordar sesión en este navegador
Iniciar sesiónIniciar sesiónCrear cuentaCrear cuenta
LWP » Foros » C/Visual C » PRE-POST CONDICIONES

C/Visual C - PRE-POST CONDICIONES

Volver
Nuevo Tema
<<>>
 
Vista:

PRE-POST CONDICIONES

Publicado por raul (6 intervenciones) el 28/08/2003 16:49:33
Hola! Necesitaría que alguien me ayudara con un problema que tengo en Visual C. Tengo que realizar las PRE- POST CONDICIONES y los INVARIANTES en una aplicación, pero no sé como realizarlos bién. Las PRE y POST casi lo tengo, pero no se como crear el INVARIANTE. Podría alguien hacerme un ejemplo? Gracias
Valora esta pregunta
Me gusta: Está pregunta es útil y esta claraNo me gusta: Está pregunta no esta clara o no es útil
0
Responder
Imágen de perfil de Alejandro

Cómo implementar invariantes en programación con Design by Contract

Publicado por Alejandro (1286 intervenciones) el 23/07/2025 22:41:46
Hola Raúl,

Entiendo que quieres aprender a implementar invariantes en tu aplicación en Visual C, en el contexto de *Design by Contract*. Los invariantes son condiciones que deben mantenerse verdaderas en todo momento para un objeto o clase, y generalmente se verifican antes y después de cada operación que modifica el estado del objeto.

Aquí te doy un ejemplo sencillo para que puedas entender cómo implementarlos:

---

Ejemplo: Clase `CuentaBancaria` con invariantes



Supongamos que tienes una clase `CuentaBancaria` con un saldo que nunca debe ser negativo.

1. Definir el invariant (invariante):

El saldo debe ser siempre >= 0.

2. Implementar métodos con verificaciones:

Antes y después de cada método que modifica el saldo, verificamos que el invariante se cumple.

---

Código ejemplo en C (simplificado):



1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
#include <stdio.h>
#include <assert.h>
 
typedef struct {
    double saldo;
} CuentaBancaria;
 
// Función para verificar el invariante
void verificarInvariante(CuentaBancaria *cuenta) {
    assert(cuenta->saldo >= 0); // Invariante: saldo >= 0
}
 
// Constructor
void inicializarCuenta(CuentaBancaria *cuenta, double saldoInicial) {
    cuenta->saldo = saldoInicial;
    verificarInvariante(cuenta); // Verificar invariantes tras inicialización
}
 
// Método para depositar
void depositar(CuentaBancaria *cuenta, double cantidad) {
    // Precondición: cantidad > 0
    assert(cantidad > 0);
 
    // Antes de modificar, verificar invariantes
    verificarInvariante(cuenta);
 
    cuenta->saldo += cantidad;
 
    // Después de modificar, verificar invariantes
    verificarInvariante(cuenta);
}
 
// Método para retirar
void retirar(CuentaBancaria *cuenta, double cantidad) {
    // Precondición: cantidad > 0
    assert(cantidad > 0);
    // Precondición: saldo >= cantidad
    assert(cuenta->saldo >= cantidad);
 
    // Verificar invariantes antes
    verificarInvariante(cuenta);
 
    cuenta->saldo -= cantidad;
 
    // Verificar invariantes después
    verificarInvariante(cuenta);
}
 
int main() {
    CuentaBancaria miCuenta;
    inicializarCuenta(&miCuenta, 100);
 
    depositar(&miCuenta, 50);
    retirar(&miCuenta, 30);
 
    printf("Saldo final: %.2f\n", miCuenta.saldo);
    return 0;
}

---

¿Qué hace este ejemplo?


- La función `verificarInvariante()` comprueba que el saldo nunca sea negativo.
- Antes y después de cada método que modifica el estado, llamamos a esa función.
- Si en algún momento el invariante se viola, `assert()` detendrá la ejecución y te alertará.

---

Resumen:


- Invariante: condición que debe mantenerse siempre.
- Implementación: crear una función que compruebe esa condición y llamarla en los puntos clave (antes y después de las operaciones que cambian el estado).
- Pre y post condiciones: también las tienes, pero en tu código ya las tienes casi listas.
Valora esta respuesta
Me gusta: Está respuesta es útil y esta claraNo me gusta: Está respuesta no esta clara o no es útil
0
Comentar