We develop a weakest-precondition-style calculus à la Dijkstra for reasoning about \emph{amortized expected runtimes of randomized algorithms with access to dynamic memory} — the $\textnormal{\textsf{aert}}$ calculus. Our calculus is truly quantitative, i.e. instead of Boolean valued predicates, it manipulates real-valued functions.

En route to the $\textnormal{\textsf{aert}}$ calculus, we study the $\textnormal{\textsf{ert}}$ calculus for reasoning about \emph{expected runtimes} of Kaminski et al. [2018] extended by capabilities for handling dynamic memory, thus enabling \emph{compositional} and \emph{local} reasoning about \emph{randomized data structures}. This extension employs \emph{runtime separation logic}, which has been foreshadowed by Matheja [2020] and then implemented in Isabelle/HOL by Haslbeck [2021]. In addition to Haslbeck's results, we further prove soundness of the so-extended $\textnormal{\textsf{ert}}$ calculus with respect to an operational Markov decision process model featuring countably-branching nondeterminism, provide extensive intuitive explanations, and provide proof rules enabling separation logic-style verification for upper bounds on expected runtimes. Finally, we build the so-called \emph{potential method} for amortized analysis into the $\textnormal{\textsf{ert}}$ calculus, thus obtaining the $\textnormal{\textsf{aert}}$ calculus. Soundness of the $\textnormal{\textsf{aert}}$ calculus is obtained from the soundness of the $\textnormal{\textsf{ert}}$ calculus and some probabilistic form of telescoping.

Since one needs to be able to handle \emph{changes in potential} which can in principle be both positive or negative, the $\textnormal{\textsf{aert}}$ calculus needs to be — essentially — capable of handling certain signed random variables. A particularly pleasing feature of our solution is that, unlike e.g. Kozen [1985], we obtain a loop rule for our signed random variables, and furthermore, unlike e.g. Kaminski and Katoen [2017], the $\textnormal{\textsf{aert}}$ calculus makes do without the need for involved technical machinery keeping track of the integrability of the random variables.

Finally, we present case studies, including a formal analysis of a randomized delete-insert-find-any set data structure [Brodal et al.\ 1996], which yields a constant expected runtime per operation, whereas no deterministic algorithm can achieve this.