Agent-Oriented Modeling by Interleaving Formal and Informal Specification