Agent-oriented modeling by interleaving formal and informal specification