Conception par contrat (DbC)

Exemple en ObjectScript

Include %occErrorsClass MyApp.Account Extends%Persistent
{

Property Balance As%Numeric;/// Deposit money into the account
Method Deposit(amount As%Numeric) As%Status
{
    // PreconditionsIf amount < 0 {
        Return$$$ERROR($$$GeneralError, "Deposit amount must be non-negative")
    }

    // Store the old balanceSet oldBalance = ..Balance// Update balanceSet..Balance = oldBalance + amount

    // PostconditionsIf (..Balance '= $$$NULLOREF) && (..Balance '= (oldBalance + amount)) {
        Return$$$ERROR($$$GeneralError, "Postcondition failed: Balance calculation error")
    }

    Quit$$$OK
}

/// Withdraw money from the account
Method Withdraw(amount As%Numeric) As%Status
{
    // PreconditionsIf amount < 0 {
        Return$$$ERROR($$$GeneralError, "Withdrawal amount must be non-negative")
    }
    If (..Balance = $$$NULLOREF) || (..Balance < amount) {
        Return$$$ERROR($$$GeneralError, "Insufficient funds")
    }

    // Store the old balanceSet oldBalance = ..Balance// Update balanceSet..Balance = oldBalance - amount

    // PostconditionsIf (..Balance '= $$$NULLOREF) && (..Balance '= (oldBalance - amount)) {
        Return$$$ERROR($$$GeneralError, "Postcondition failed: Balance calculation error")
    }

    Quit$$$OK
}

/// Invariant: Balance should always be non-negative
Method CheckBalanceInvariant() As%Status
{
        Set tSC = $$$OKIf..Balance < 0 {
            Set tSC = $$$ERROR($$$GeneralError, "Balance invariant violated: Balance is negative")
        }
        Quit tSC
}

/// Class method to test the Account classClassMethod TestAccount() As%Status
{
    // Create a new instance of AccountSet account = ##class(MyApp.Account).%New()
    
    // Initialize the balanceSet account.Balance = 0// Test depositing a positive amountSet tSC = account.Deposit(100)
    If$$$ISERR(tSC) {
        Write"Deposit failed: ", $system.Status.GetErrorText(tSC), !
        Quit tSC
    }
    Write"Deposit succeeded: Balance after deposit: ", account.Balance, !
    
    // Test depositing a negative amount (should fail)Set tSC = account.Deposit(-50)
    If$$$ISERR(tSC) {
        Write"Deposit of negative amount failed as expected: ", $system.Status.GetErrorText(tSC), !
    } Else {
        Write"Deposit of negative amount unexpectedly succeeded", !
        Quit$$$ERROR($$$GeneralError, "Deposit of negative amount unexpectedly succeeded")
    }
    
    // Test withdrawing a valid amountSet tSC = account.Withdraw(50)
    If$$$ISERR(tSC) {
        Write"Withdrawal failed: ", $system.Status.GetErrorText(tSC), !
        Quit tSC
    }
    Write"Withdrawal succeeded: Balance after withdrawal: ", account.Balance, !
    
    // Test withdrawing more than the available balance (should fail)Set tSC = account.Withdraw(200)
    If$$$ISERR(tSC) {
        Write"Withdrawal of more than available balance failed as expected: ", $system.Status.GetErrorText(tSC), !
    } Else {
        Write"Withdrawal of more than available balance unexpectedly succeeded", !
        Quit$$$ERROR($$$GeneralError, "Withdrawal of more than available balance unexpectedly succeeded")
    }
    
    // Check balance invariant (should succeed)Set tSC = account.CheckBalanceInvariant()
    If$$$ISERR(tSC) {
        Write"Balance invariant violated: ", $system.Status.GetErrorText(tSC), !
        Quit tSC
    }
    Write"Balance invariant holds true", !
    
    // Intentionally set balance to negative value to trigger balance invariant failureSet account.Balance = -10// Check balance invariant (should fail)Set tSC = account.CheckBalanceInvariant()
    If$$$ISERR(tSC) {
        Write"Balance invariant violated as expected: ", $system.Status.GetErrorText(tSC), !
    } Else {
        Write"Balance invariant unexpectedly held true", !
        Quit$$$ERROR($$$GeneralError, "Balance invariant unexpectedly held true")
    }
    
    Write"Account operations completed successfully", !
    Quit$$$OK
}

Storage Default
{
<Data name="AccountDefaultData">
<Value name="1">
<Value>%%CLASSNAME</Value>
</Value>
<Value name="2">
<Value>Balance</Value>
</Value>
</Data>
<DataLocation>^MyApp.AccountD</DataLocation>
<DefaultData>AccountDefaultData</DefaultData>
<IdLocation>^MyApp.AccountD</IdLocation>
<IndexLocation>^MyApp.AccountI</IndexLocation>
<StreamLocation>^MyApp.AccountS</StreamLocation>
<Type>%Storage.Persistent</Type>
}

}

Exemple en Python :

classAccount:def__init__(self):
        self.balance = 0defdeposit(self, amount):if amount < 0:
            raise ValueError("Deposit amount must be non-negative")
        
        old_balance = self.balance
        self.balance += amount
        
        # Postconditionsif self.balance != old_balance + amount:
            raise ValueError("Postcondition failed: Balance calculation error")

    defwithdraw(self, amount):if amount < 0:
            raise ValueError("Withdrawal amount must be non-negative")
        if self.balance < amount:
            raise ValueError("Insufficient funds")

        old_balance = self.balance
        self.balance -= amount
        
        # Postconditionsif self.balance != old_balance - amount:
            raise ValueError("Postcondition failed: Balance calculation error")

    defcheck_balance_invariant(self):if self.balance < 0:
            raise ValueError("Balance invariant violated: Balance is negative")

    @classmethoddeftest_account(cls):
        account = cls()
        
        try:
            # Test depositing a positive amount
            account.deposit(100)
            print("Deposit succeeded: Balance after deposit:", account.balance)
            
            # Test depositing a negative amount (should fail)
            account.deposit(-50)
        except ValueError as e:
            print("Deposit of negative amount failed as expected:", e)
        else:
            raise ValueError("Deposit of negative amount unexpectedly succeeded")
        
        try:
            # Test withdrawing a valid amount
            account.withdraw(50)
            print("Withdrawal succeeded: Balance after withdrawal:", account.balance)
            
            # Test withdrawing more than the available balance (should fail)
            account.withdraw(200)
        except ValueError as e:
            print("Withdrawal of more than available balance failed as expected:", e)
        else:
            raise ValueError("Withdrawal of more than available balance unexpectedly succeeded")
        
        try:
            # Check balance invariant (should succeed)
            account.check_balance_invariant()
            print("Balance invariant holds true")
        except ValueError as e:
            print("Balance invariant violated:", e)
        
        # Intentionally set balance to negative value to trigger balance invariant failure
        account.balance = -10try:
            # Check balance invariant (should fail)
            account.check_balance_invariant()
        except ValueError as e:
            print("Balance invariant violated as expected:", e)
        else:
            raise ValueError("Balance invariant unexpectedly held true")
        
        print("Account operations completed successfully")

# Run the test
Account.test_account()