Abstract
Formal methods are mathematical techniques use in design, development and verification of software and hardware system. Geographic information systems GIS use to collect, store, analyze and present spatial informations. GIS databases are usually very complex to design. Formal methods can play an important role in their design. In the paper, the authors investigate an approach of formal specification of spatial databases for GIS systems using Z notation (a formal language with a powerful structuring mechanism). For the purpose, we use an example from the context of GIS and spatial database to draw Entity Relationship Diagram ERD. Further the paper presents transformation from Entity Relationship Diagram ERD to formal specification that shows all the entities and their relationships in Z notation. In this paper we exhibit that the approach is applicable for spatial database designing. Consequently this leads to unambiguous, consistent and verified GIS system.