This innovative volume provides a hands-on introduction to techniques for specifying the behavior of software components. Featured topics include techniques for using programmer-friendly assertional notations to specify, develop, and verify small but nontrivial algorithms and data representations and for using state diagrams, grammars, and regular expressions to specify and develop recognizers for formal languages. The presentation is based on numerous examples and case studies. It is appropriate for second- and third-year computer science and computer engineering students familiar with basic concepts of discrete mathematics and logic. Using this book will help readers improve their programming skips and develop a solid foundation for subsequent courses in advanced algorithms and data structures, software design, formal methods, compilers, programming languages, and theory.