From natural language requirements to formal descriptions in Alloy through boilerplates Teses