Editing Abstraction (computer science) (section)

==Considerations==
When discussing [[formal semantics of programming languages]], [[formal methods]] or [[abstract interpretation]], ''abstraction'' refers to the act of considering a less detailed, but safe, definition of the observed program behaviors. For instance, one may observe only the final result of program executions instead of considering all the intermediate steps of executions. Abstraction is defined to a ''concrete'' (more precise) model of execution.

Abstraction may be ''exact'' or ''faithful'' with respect to a property if one can answer a question about the property equally well on the concrete or abstract model. For instance, if one wishes to know what the result of the evaluation of a mathematical expression involving only integers +, -, ×, is worth [[modular arithmetic|modulo]] ''n'', then one needs only perform all operations modulo ''n'' (a familiar form of this abstraction is [[casting out nines]]).

Abstractions, however, though not necessarily ''exact'', should be ''sound''. That is, it should be possible to get sound answers from them—even though the abstraction may simply yield a result of [[undecidable problem|undecidability]]. For instance, students in a class may be abstracted by their minimal and maximal ages; if one asks whether a certain person belongs to that class, one may simply compare that person's age with the minimal and maximal ages; if his age lies outside the range, one may safely answer that the person does not belong to the class; if it does not, one may only answer "I don't know".

The level of abstraction included in a programming language can influence its overall [[usability]]. The [[Cognitive dimensions]] framework includes the concept of ''abstraction gradient'' in a formalism. This framework allows the designer of a programming language to study the trade-offs between abstraction and other characteristics of the design, and how changes in abstraction influence the language usability.

Abstractions can prove useful when dealing with computer programs, because non-trivial properties of computer programs are essentially [[undecidable problem|undecidable]] (see [[Rice's theorem]]). As a consequence, automatic methods for deriving information on the behavior of computer programs either have to drop termination (on some occasions, they may fail, crash or never yield out a result), soundness (they may provide false information), or precision (they may answer "I don't know" to some questions).

Abstraction is the core concept of [[abstract interpretation]]. [[Model checking]] generally takes place on abstract versions of the studied systems.