One of the key challenges in using formal methods is producing accurate formalizations of natural language requirements, as providing incorrect formalizations may miss bugs or even codify their existence. Yet despite this critical role, recent studies have revealed that even experienced experts make mistakes when formalizing relatively simple specifications in Linear Temporal Logic (LTL).
We analyze the data from one recent study from the perspective of linguistic pragmatics — the systems by which words carry additional non-explicit meaning. We find that nearly half of novice mistakes and 80% of expert mistakes in the dataset could be explained by misunderstanding whether and when these enrichments of what is said with additional meaning should be formalized. We conclude that further study of the relationship between natural language specifications and pragmatics has potential to reduce misformalizations.
Jiangping Huang Chongqing University of Posts and Telecommunications, Dongming Jin Peking University, China, Weisong Sun Nanyang Technological University, Yang Liu Nanyang Technological University, Zhi Jin Peking University
