In software engineering, software is developed following a development process which includes phases such as requirements analysis, design and implementation, with validation and verification - mostly testing - done along the way. To have a more formal and dependable approach to functionally correct software development, we need an automated approach that generates code from original requirements given in natural language. In this paper we give an overall idea of how this can (even if partially) be achieved using logic, more concretely first-order logic as used in the constraint solver Alloy.
School of Informatics and Computing, Indiana University.