Temporal logics cover important classes of system specifications dealing with system behavior over time. Despite the prevalence of long-running systems that accept repeated input and output, and thus the clear relevance of temporal specifications to training software engineers, temporal logics are rarely taught to undergraduates. We motivate and describe an approach to teaching temporal specifications and temporal reasoning indirectly through teaching students about \emph{mocking dependencies}, which is widely used in software testing of large systems (and therefore of more obvious relevance to students), less notationally intimidating to students, and still teaches similar reasoning principles. We report on 7 years of experience using this indirect approach to behavioral specifications in a software quality course.

@inproceedings{splashe24, author = {Gordon, Colin S.}, title = {Mocking Temporal Logic}, abbr = {SPLASH-E}, booktitle = {SPLASH-E}, year = {2024}, address = {Pasadena, California, USA}, month = {October}, doi = {10.1145/3689493.3689980}, bibtex_show = {true}, abstract = { Temporal logics cover important classes of system specifications dealing with system behavior over time. Despite the prevalence of long-running systems that accept repeated input and output, and thus the clear relevance of temporal specifications to training software engineers, temporal logics are rarely taught to undergraduates. We motivate and describe an approach to teaching temporal specifications and temporal reasoning indirectly through teaching students about \emph{mocking dependencies}, which is widely used in software testing of large systems (and therefore of more obvious relevance to students), less notationally intimidating to students, and still teaches similar reasoning principles. We report on 7 years of experience using this indirect approach to behavioral specifications in a software quality course. }, }