The study of open irredundant sets of vertices in a graph is of interest from both practical and theoretical perspectives. On the one hand, such sets correspond to possible groups of simultaneous senders in broadcast networks. On the other, their maximum size represents a new parameter on graphs. Computing a maximum irredundant set in an arbitrary graph is known to be difficult. This motivates development of an efficient algorithm on tree-structured graphs. Here, we present and prove correct such an algorithm, emphasizing a development technique whereby a general algorithm is specialized for the problem at hand, proven correct, and then refined to reduce its complexity.