Design By Contract (DbC)
Discussion (1)0
Comments
Thank you @Herman Slagman !
I like your suggestion and would fully support it if ISC would take that turn.
You mentioned ignorance and you are right. I'm full with you.
Though I still see another more dangerous hurdle to pass:
- Understanding the concept. Applying the concept. Teaching the concept.
I just fear there might not be enough qualified developers available to execute it.
Seeing the actual situation on my side of the globe I wouldn't expect to find enough experts.
Very good point @Herman Slagman
To illustrate your point, in 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>
}
}
With the following results :
write##class(MyApp.Account).TestAccount()
Deposit succeeded: Balance after deposit: 100
Deposit of negative amount failed as expected: ERROR #5001: Deposit amount must be non-negative
Withdrawal succeeded: Balance after withdrawal: 50
Withdrawal of more than available balance failed as expected: ERROR #5001: Insufficient funds
Balance invariant holds true
Balance invariant violated as expected: ERROR #5001: Balance invariant violated: Balance is negative
Account operations completed successfully
1In 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()
With the following results :
python account.py
Deposit succeeded: Balance after deposit: 100
Deposit of negative amount failed as expected: Deposit amount must be non-negative
Withdrawal succeeded: Balance after withdrawal: 50
Withdrawal of more than available balance failed as expected: Insufficient funds
Balance invariant holds true
Balance invariant violated as expected: Balance invariant violated: Balance is negative
Account operations completed successfully