Ag is a specification language presented as a syntactic sugaring of the First-Order Dynamic Logic of Fork Algebras. This language is particularly attractive due to its expressive power, easy-to-understand semantics, and the existence of a complete deductive system. The example shows how the language has been embedded in PVS, providing a semantic framework for reasoning about Ag specifications. A simple cache system is then specified as a case study. You must have PVS version 3.1 or later to use this.