High integrity Ada the SPARK - Barnes (Addison-Wesley, 1997)