I've been of the impression that using formal methods would be tedious and difficult, and yet would primarily be useful or important for complicated concurrent utilities such as transactional databases.
Thus, as an application developer, I'd use services such as a database which perhaps itself might make use of formal methods in its implementation, but formal methods wouldn't be relevant for me directly.
However, how do I know when I'm using a service such as a transactional database correctly?
For example, suppose I query the balance of my checking and savings accounts to find out how much money I have. Naturally, if I were to do that query in a single transaction I'd get the right total, but if I were to incorrectly query the checking account and savings account balances in separate transactions I could get the wrong answer if a transfer happened to occur between queries.
1. start with $300 in checking and $700 in savings
2. query checking account balance: $300
3. transfer $100 from savings to checking
4. query savings account balance: $600
5. my calculated total: $900
This is obvious in a simple example, but in a more complicated situation I might not notice that I haven't set the boundaries of my transaction correctly.
How to find out if my code is correct?
I have the classic concurrent code dilemma of not being able to rely on testing (it's unlikely that a transfer will happen at just the wrong moment for the bug to be demonstrated), nor on inspection (each part of the code looks fine, it's only when one notices that the combination is incorrect that one can see that there's a problem).
Can formal methods help? Would they be difficult?
To look at a concrete implementation, in _javascript_ programming,
promises have been becoming popular.
E.g.,
Promise.join(
fetch_checking_balance(),
fetch_savings_balance(),
function (checking, savings) {
report(checking + savings);
}
);
asynchronously and simultaneously fetches the two balances (such as by making API calls), and, when both results are available, reports their sum.
A promise is said to be "fulfilled" when it has a value. Thus fetch_checking_balance and fetch_savings_balance both return a promise, Promise.join waits until both have been fulfilled, and then calls the function in its last argument with the values of the promises.
(Promises can also be rejected with an error; and Promise.join will return a rejected promise if and as soon as any of its input promises reject, without waiting for the rest to complete. I don't model rejected promises in this example though).
It looks like that waiting for a promise to be fulfilled can be easily and naturally modeled in Pluscal by using the await statement:
--algorithm Balance {
variables
\* checking account and savings account balances as stored in the database
db_a = initialA;
db_b = initialB;
\* promises
a_fulfilled = FALSE; a_value = notset;
b_fulfilled = FALSE; b_value = notset;
join_fulfilled = FALSE; join_value = notset;
define {
total == 1000
initialA == 300
initialB == total - initialA
transferAmount == 100
notset == {}
}
process ( Transfer = "transfer" )
{
L1: db_a := db_a + transferAmount ||
db_b := db_b - transferAmount;
};
process ( FetchA = "fetch_a" )
{
L2: a_fulfilled := TRUE || a_value := db_a;
}
process ( FetchB = "fetch_b" )
{
L3: b_fulfilled := TRUE || b_value := db_b;
}
process ( Join = "join" )
{
L4: await a_fulfilled /\ b_fulfilled;
join_fulfilled := TRUE || join_value := << a_value, b_value >>;
}
process ( Report = "report" )
{
L5: await join_fulfilled;
assert(LET a == join_value[1]
b == join_value[2]
IN a + b = total)
}
}
What's nice about this is that it's nearly a mechanical translation of the original promise code into Pluscal.
Running this in Pluscal immediately finds the cases where the assertion fails (when the calculated total is incorrect).
This is my first attempt so I don't know if such an approach would turn out to be practical for substantive programs. I was pleasantly pleased however that it turned out to be so straightforward.
Andrew