Consider the Z specification for bank account system in my pics. Analyze each of the following four operation schemas, and identify their pre and post-conditions:-

-Deposit (should allow depositing any amount into the account)

-Withdraw (should allow withdrawal such that the minimum balance remains Rs. 1000)

-Inquire (to check current balance of the account)

-Open a new account

If you think precondition of an operation schema does not cover all possible cases, define additional operation schemas to cover the missing pre-conditions.

 

ACCOUNT,PERSON,ACCNUM,BALANCE,TYPE:N Bank Account Operation Today, OpeationLimmit,AccHolder, CreditLimmit:N AccHolder: ACCOUNT PERSON Credit:ACCNUMBALANCE Account:Z NewAcccount: Y AccountType:TYPE dom AccHolder= Account Y= 2 Credit 0 Credit