Modular verification of concurrent systems
Ann E. Kelley Sobel · OhioLink ETD Center (Ohio Library and Information Network) · 1986
statem en t S is operationally valid A Implies B; A d B Universal quantifier Existential quantifier Replace each occurrence of x w ith e in th e assertion p A sequence An elem ent of a sequence C oncatenate the elem ent to th e right end of h T h e sequence consisting of th e »*fc through kth elem ents o f h The length of h h i is an initial subsequence o f h i