Big Number Addition
In this chapter we consider an example programming problem and its solution in Piton. The problem is to specify, implement, and verify a program for doing “big number addition.” This chapter is a rather long but instructive detour from our main goal of implementing Piton on FM9001 and proving the implementation correct.
KeywordsData Segment Data Area Main Program Symbolic Execution Program Counter
Unable to display preview. Download preview PDF.