پردازش مستقیم زبان طبیعی برای درک نیازهای نرم افزار منجر به ایجاد ابهاماتی خواهد شد. این ابهامات در نهایت بر کیفیت نرم افزار نهایی تاثیر منفی خواهند گذاشت. بکارگیری متدهای رسمی باعث کاهش این ابهامات در توصیف نیازهای نرم افزار خواهد شد. در این مقاله زبان توصیف رسمی Z را برای توصیف وب سایت مرامی سوار بکاربرده ایم. این وب سایت با هدف یافتن همسفر برای رانندگان بین شهری طراحی شده است. همچنین مسافرینی که قصد سفر با هزینه کمتر را دارند می توانند با استفاده از این برنامه، رانندگان هم مسیر خود را بیابند. استفاده از زبان Z منجر به افزایش دقت در توصیف نیازها خواهد شد. این وب سایت ابتدا با زبان UML مدلسازی شده و نمودار مورد-کاربرد آن بدست آمده است. سپس از توصیف های Z برای کاهش هرچه بیشتر ابهامات استفاده شده است. ارزیابی توصیف های رسمی Z با استفاده از ابزار Z\EVES صورت پذیرفته است. درستی تمامی شماهای طراحی شده، با استفاده از Z\EVES اثبات شده است.
