Abstract
A second-order axiomatization of dynamic logic with array assignments is presented. This axiomatization is shown to be arithmetically complete in the sense of Harel. As an example, a partial correctness assertion concerning a sorting algorithm is proved.
Get full access to this article
View all access options for this article.