{-

A simple database example. 

Here is a simple uPL script to clean up a database of customer's
accounts. If a customer have no positive accounts then all his
accounts will be deleted. The post-condition certifies that the update
is safe: for any customer, the sum of all his positive saldos will
remain unchanged.

-}

prog cleanup ( db  :: & [Record {Id :: String; Saldo :: Int}]
	     ; customerId :: String
	     )

numOfPosAccount :: Int

pre T

do {

numOfPosAccount := cnt (select 0
			  from  s <- db
			  where (s.Id = customerId) /\ s.Saldo > 0) ;

if numOfPosAccount>0
    then skip
    else db := deleteById customerId db
}

post

(!customer :- T -:
	sumOfPositiveSaldo customer db
	=
	sumOfPositiveSaldo customer db__0)

lconst

deleteById         :: String 
			-> [Record {Id :: String; Saldo :: Int}]
			-> [Record {Id :: String; Saldo :: Int}] ;

sumOfPositiveSaldo :: String 
			-> [Record {Id :: String; Saldo :: Int}]
			-> Int