Formal contracts and assertions are effective methods to enhance software quality by enforcing preconditions, postconditions, and invariants. Previous research has demonstrated the value of contracts in traditional software development contexts. However, the adoption and impact of contracts in the context of mobile application development, particularly of Android applications, remain unexplored. To address this, we present the first large-scale empirical study on the presence and use of contracts in Android applications, written in Java or Kotlin. We consider different types of contract elements divided into five categories: conditional runtime exceptions, APIs, annotations, assertions, and other. We analyzed 2,390 Android applications from the F-Droid repository and processed more than 51,749 KLOC to determine 1) how and to what extent contracts are used, 2) how contract usage evolves, and 3) whether contracts are used safely in the context of program evolution and inheritance. Our findings include: 1) although most applications do not specify contracts, annotation-based approaches are the most popular among practitioners; 2) applications that use contracts continue to use them in later versions, but the number of methods increases at a higher rate than the number of contracts; and 3) there are many potentially unsafe specification changes when applications evolve and in subtyping relationships, which indicates a lack of specification stability. Our findings show that it would be desirable to have libraries that standardize contract specifications in Java and Kotlin, and tools that aid practitioners in writing stronger contracts and in detecting contract violations in the context of program evolution and inheritance.

翻译：形式化合约与断言通过强制前置条件、后置条件和不变量，是提升软件质量的有效方法。先前研究已证明合约在传统软件开发环境中的价值。然而，合约在移动应用开发（特别是Android应用）中的采用情况与影响仍未被探索。为此，我们首次对Android应用（使用Java或Kotlin编写）中合约的存在与使用进行了大规模实证研究。我们将不同类型的合约元素分为五类：条件运行时异常、API、注解、断言及其他。我们分析了F-Droid仓库中的2,390个Android应用，处理超过51,749千行代码，以确定：1) 合约的使用方式与程度；2) 合约使用如何演进；以及3) 在程序演进与继承背景下合约是否被安全使用。研究发现包括：1) 尽管大多数应用未规定合约，但基于注解的方法在从业者中最受欢迎；2) 使用合约的应用在后续版本中继续使用，但方法数量的增速高于合约数量的增速；3) 在应用演进及子类型关系中存在许多潜在不安全的规约变更，表明规约稳定性不足。我们的发现表明，有必要开发标准化Java和Kotlin合约规约的库，以及帮助从业者编写更强合约并在程序演进与继承背景下检测合约违反的工具。