Abstract
Geometric algorithms can present significant challenges for formal methods. We describe the formalization and verification of an algorithm posing such challenges. Given two overlapping polygons A and B, the Polygon Merge algorithm derives a new polygon whose edges are outermost, partial edges of A and B. The algorithm has been verified to satisfy correctness criteria expressed as two point-set properties. We have constructed a rigorous proof using the PVS interactive theorem prover along with support from the NASA PVS Library. While the algorithm itself is fairly compact, its proof was a moderately complicated undertaking. Owing to the complexity of reasoning about the spatial relationships of two different polygons, the proof required hundreds of supporting lemmas. Most of the definitions and lemmas introduced were needed to build a body of deductive artifacts sufficiently robust for this problem domain. Many of these artifacts will be generally useful for working with polygons, line segments and 2D vectors. Accordingly, we are distilling these products into a reusable PVS library.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bertot, Y.: Formal verification of a geometry algorithm: a quest for abstract views and symmetry in Coq proofs. In: Fischer, B., Uustalu, T. (eds.) ICTAC 2018. LNCS, vol. 11187, pp. 3–10. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02508-3_1
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press and McGraw-Hill, Cambridge (2009)
Graham, R.L.: An efficient algorithm for determining the convex hull of a finite planar set. Inf. Process. Lett. 1(4), 132–133 (1972)
Hocking, A.B., Rowanhill, J.C., Di Vito, B.L.: An analysis of implementing PVS in SPARK Ada. In: 2020 IEEE/AIAA 39th Digital Avionics Systems Conference (DASC). IEEE (2020)
Hormann, K., Agathos, A.: The point in polygon problem for arbitrary polygons. Comput. Geom. 20(3), 131–144 (2001)
Kong, H., Zhang, H., Song, X., Gu, M., Sun, J.: Proving computational geometry algorithms in TLA+2. In: 5th IEEE International Conference on Theoretical Aspects of Software Engineering (TASE 2011). IEEE (2011)
Margalit, A., Knott, G.D.: An algorithm for computing the union, intersection or difference of two polygons. Comput. Graph. 13(2), 167–183 (1989)
NASA: PolyCARP. https://github.com/nasa/PolyCARP
NASA Langley Research Center: PVS library collection, theories and proofs. http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/
Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_217
Shimrat, M.: Algorithm 112: position of point relative to polygon. Comm. ACM 5(8), 434 (1962)
Zalik, B.: Merging a set of polygons. Comput. Graph. 25(1), 77–88 (2001)
Acknowledgments
This work was funded by USAF AFRL/RQQA contract FA8650-17-F-2220. Approved for Public Release: Distribution Unlimited (Case Number: 88ABW-2020-3765).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Di Vito, B.L., Hocking, A.B. (2021). Polygon Merge: A Geometric Algorithm Verified Using PVS. In: Dutle, A., Moscato, M.M., Titolo, L., Muñoz, C.A., Perez, I. (eds) NASA Formal Methods. NFM 2021. Lecture Notes in Computer Science(), vol 12673. Springer, Cham. https://doi.org/10.1007/978-3-030-76384-8_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-76384-8_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-76383-1
Online ISBN: 978-3-030-76384-8
eBook Packages: Computer ScienceComputer Science (R0)