Invariant-Based Automatic Testing of AJAX User Interfaces