Detecting Assumptions on Deterministic Implementations of Non-deterministic Specifications

摘要: Some commonly used methods have nondeterministicspecifications, e.g., iterating through a set canreturn the elements in any order. However, non-deterministicspecifications typically deterministic implementations, e.g.,iterating two sets constructed same way mayreturn their We use termADINS code to refer that Assumes DeterministicImplementation of method with Non-deterministic Specification. Such ADINS can behave unexpectedly whenthe implementation changes, even if specification remainsthe same. Further, lead flaky tests -- teststhat pass or fail seemingly non-deterministically. present simple technique, called NONDEX, for detectingflaky due code. implemented NONDEX forJava: we found 31 non-deterministic specificationsin Java Standard Library, manually built non-deterministicmodels these methods, and modified VirtualMachine explore various choices. evaluatedNONDEX on 195 open-source projects from GitHub 72student submissions programming homework assignment.NONDEX detected 60 21 and110 34 student submissions.