Abstraction and verification in Alphard : design and verification of a tree handler

The design of t h e A l p h a r d programming l a n g u a g e has b e en strongly i n f l u e n c e d by ideas from the areas of p r o g r a m m i ng methodology and formal p r o g r a m verification . The i n t e r a c t i o n of t h e s e ideas and their i n f l u e n c e on A l p h a r d are d e s c r i b e d by developing a n o n t r i v i a l example , a p r o g r a m for m a n i p u l a t i n g the p a r s e tree of an a r i t h m e t i c expression.